An integrated system for solving, proving, and checking
Axeyum contains five native components written in Rust: its own SAT solver, SMT solver, proof-carrying computer algebra system, Lean-core proof kernel, and dependency-aware formal library.
The Axeyum SMT Solver starts with typed terms and lowers supported queries through theory solving or bit-blasting. The Axeyum SAT Solver provides the CDCL decision layer. The Axeyum CAS implements exact symbolic algorithms and operation-specific checks. The Axeyum Kernel checks a selected Lean-core profile. The Axeyum Library records accepted facts and their dependencies.
Axeyum is an independent implementation. We benchmark its solver against Z3, cvc5, and Bitwuzla. We compare its computer algebra system with Mathematica and SymPy, its proof checker with Lean, and its formal library with mathlib. None of these systems runs inside Axeyum.
03ae4a3c9 Measured Source Source build only 
Axeyum chooses an open statement, gathers relevant facts, produces a candidate result, checks the evidence, and records the accepted fact. The new fact can support later work.
Axeyum records proof dependencies as a directed acyclic graph, or DAG. Each arrow leads from a prerequisite to a result that uses it. There is no circular chain of justification: a proof cannot depend on itself.
The research cycle repeats as this graph grows. A missing prerequisite identifies work that could make a larger proof possible. The intermediate and extreme value theorems show how separate parts of the library contribute to a result.
The approximate Intermediate Value Theorem (IVT) combines repeated bisection, a bound on how fast the interval shrinks, and a continuity bound. Together they establish a point where the function is as close to zero as requested.
The approximate Extreme Value Theorem (EVT) builds on a supremum: the least upper bound of the function's values. Its earlier proofs supply both an upper bound and points close to it. Chaining these bounds gives an approximate maximum.
The real-number decay bound used by IVT also supports a geometric-series estimate. The same proved inequality can supply a missing step in a different development.
A calculus example
Suppose an object's position after t seconds is p(t) = t³. Its average velocity from 0 to 3 seconds is 9. The Mean Value Theorem says its instantaneous velocity must equal 9 at some time in that interval.
Axeyum finds the exact time c = √3, rather than a decimal estimate. A separate checker recomputes the average velocity, differentiates the polynomial, proves 1 < c < 2, and checks p'(c) = 9. The ledger records the accepted certificate for later use.
position p(t) = t³
interval 0 ≤ t ≤ 3
average rate (p(3) - p(0)) / 3 = 9
exact witness c = √3, with 1 < c < 2
checked result p'(c) = 3c² = 9Axeyum does not yet match these systems in their strongest areas. Its solver has less coverage than Z3, cvc5, and Bitwuzla. Its proof environment and library are much smaller than Lean and mathlib.
The complete process works, but automated production remains limited. The comparison reports state coverage, speed, disagreements, checked terms, and axiom footprints.
The complete process works. Autonomous production remains limited. Each result below names its measurement and its main limit.
| Area | Current result | Evidence | Limit |
|---|---|---|---|
| Solver | 762 of 992 files decided across 24 logic fragments | 674 decisions compared with z3 4.13.3; 0 disagreements | QF_NIA parity ledger, 2026-09-11: Axeyum decides 41 of 200 files and cvc5 1.3.4 decides 87. An Axeyum-only A/B on 2026-09-17, not a ledger entry, decides 87 of the same files |
| Evidence | 93 of 130 QF_BV unsat results have accepted certificates | 79 certificates rechecked from serialized text | 37 unsat results have no certificate from the evidence run |
| Kernel | 2,584 of 2,586 kernel-route facts have an empty axiom footprint | Kernel::axiom_footprint and the fact validator | No interactive goal state, tactic language, or general Lean elaborator |
| Library | 2,676 distinct propositions established from 2,971 checked facts | python3 scripts/validate-facts.py @ 03ae4a3c9, 2026-10-05 | 267 open facts and a large external classification backlog |
| Knowledge production | One admitted result made one descendant newly ready in the recorded example | docs/autogenesis/76-exact-fibonacci-coprimality-admission.md @ 03ae4a3c9 | Reusable autonomous production remains small |
Build the source, check the fact ledger, and replay the recorded Fibonacci result.
$ git clone https://github.com/mjbommar/axeyum.git
$ cd axeyum
$ python3 scripts/validate-facts.py
$ python3 scripts/check-autogenesis-fact-operation.py \
--fact artifacts/facts/F-ml430-nat-fib-coprime-fib-succ-162fc738.json