Axeyum
Get started
Vision
Learn
By fieldSATSMTComputer algebraProof checkingFormal librariesConcept wiki
Components
SAT SolverSMT SolverCASKernelLibrary
Problems
Results
SMT-LIB benchmarksCAS comparisonLean comparisonmathlib comparison
Artifacts
Docs
SearchGet startedGitHub ↗

Getting started

Choose where to begin

Axeyum uses different components for Boolean choices, typed constraints, symbolic expressions, proof terms, and formal knowledge. These lessons explain each component from its basic terms through a worked problem.

Start with lesson 1 Open the concept index

Find your starting point

Start with the form of the problem

Use Lesson 1 if formal reasoning is new to you. Otherwise, identify the kind of object in your problem and open the matching component lesson.

A formal question leads to one of five lesson groups: Boolean choices lead to SAT, typed constraints lead to SMT, symbolic expressions lead to computer algebra, proof terms lead to the proof kernel, and accepted facts lead to the formal library. What kind of formal object do you need to reason about? Boolean choices SAT Can any assignment satisfy every Boolean constraint? Lesson 3 → Typed constraints SMT Can values satisfy arithmetic, arrays, or bit-vectors? Lesson 4 → Symbolic expressions Computer algebra Can an expression be rewritten, differentiated, or integrated? Lessons 5 and 6 → Proof terms Proof kernel Does this term prove the stated proposition? Lessons 7 and 8 → Accepted facts Formal library Which facts and assumptions support this result? Lessons 9 and 10 → Start with Lesson 1 if claims, constraints, and evidence are new to you.

What kind of formal object do you need to reason about?

Boolean choices SAT Can any assignment satisfy every Boolean constraint? Lesson 3 → Typed constraints SMT Can values satisfy arithmetic, arrays, or bit-vectors? Lesson 4 → Symbolic expressions Computer algebra Can an expression be rewritten, differentiated, or integrated? Lessons 5 and 6 → Proof terms Proof kernel Does this term prove the stated proposition? Lessons 7 and 8 → Accepted facts Formal library Which facts and assumptions support this result? Lessons 9 and 10 →

Start with Lesson 1 if claims, constraints, and evidence are new to you.

Choose the form of the problem first. Each lesson defines its terms and links to the Axeyum component that implements the operation.

Reading order

Use the sequence or choose one component

The complete sequence supplies the background for each later lesson. A reader who already knows Boolean logic can start with SAT or SMT. Each component lesson links back to the exact terms it uses and forward to the implementation and result pages.

A lesson develops several related ideas through a worked problem. A concept article defines one term and records its examples, distinctions, and connections.

Choose by field

Start with the work you already know

Field guides describe the results available now, why they matter to that field, and the work that can extend the current base.

Open all field guides →
Number theoryConstructive analysisClassical analysisAlgebraGeometryTopologyCombinatoricsProbability and statistics See every field →

01

Part 1

Formal questions

  1. Lesson 1 How a rule becomes a checkable problem What must we write down before a program can check a claim?
  2. Lesson 2 From yes-or-no rules to Boolean formulas How can a set of ordinary yes-or-no rules become one exact formula?

02

Part 2

SAT and SMT

  1. Lesson 3 How a SAT solver searches How can a program rule out enormous numbers of Boolean assignments? sat
  2. Lesson 4 Adding arithmetic and machine values What changes when constraints contain integers, strings, or fixed-width arithmetic? smt

03

Part 3

Computer algebra

  1. Lesson 5 Expressions as mathematical objects What can a program learn by keeping variables instead of replacing them with numbers?
  2. Lesson 6 How Axeyum checks symbolic results How can a large computation return evidence that smaller code can check? cas

04

Part 4

Proof checking

  1. Lesson 7 Why a proof can be a term How can a proof checker treat logic as a form of typed programming?
  2. Lesson 8 What the Axeyum Kernel checks Which judgments belong inside a proof kernel, and which services belong outside it? kernel

05

Part 5

Formal knowledge

  1. Lesson 9 How a formal library reuses checked facts What must a library retain so that one checked result can support another? library
  2. Lesson 10 Constructive and classical assumptions Why can two formal proofs of familiar mathematics have different axiom footprints? library
  3. Lesson 11 How the Axeyum components work together How can search, computation, proof checking, and stored knowledge share one system without sharing one checker?

Choose by system

Five components, five kinds of work

Boolean satisfiability (SAT)Decide Boolean constraints. Satisfiability modulo theories (SMT)Decide constraints with theories such as arithmetic and bit-vectors. Computer algebraCompute exact symbolic results and check operation-specific evidence. Proof kernelCheck explicit proof terms and declaration dependencies. Formal libraryRetain facts, evidence, assumptions, and dependency edges.