How it works
Axeyum implements its own SAT solver, SMT solver, proof-carrying computer algebra system, Lean-core proof kernel, and dependency-aware formal library.
Axeyum's default reasoning path runs its own Rust code. Z3, cvc5, Bitwuzla, Mathematica, SymPy, Lean, and mathlib do not run as hidden engines. Selected external solvers are optional, feature-gated tools for differential testing and benchmark comparisons.
These research implementations include complete native routes on selected fragments. Their breadth, performance, interfaces, and user ecosystems remain smaller than those of the established systems.
Axeyum chooses an open statement, gathers relevant facts, produces a candidate result, checks its evidence, and records the accepted fact. The dependency graph can then make related work available.
Proposal
The SMT solver returns models, verdicts, and certificates. The computer algebra system returns symbolic results with operation-specific checks. Proof producers construct terms for the selected Lean-core profile.
Native solvers and imported material may supply comparison data or candidates. Their output does not receive a stronger status until the selected Axeyum route checks it.
Checking
A sat result uses model replay against the original terms. Selected
unsat routes use DRAT, Farkas, Alethe, or specialized certificates. Computer algebra
operations use exact checks such as substitution or multiplication.
Evidence from one route does not certify another route. The ledger records the exact checker and the assumptions required for each result.
Admission
The Rust kernel implements a selected Lean-core profile. It checks dependent terms, universes, reduction, definitional equality, inductives, recursors, and proof irrelevance. It computes each admitted declaration's dependencies and axiom footprint.
The kernel has no interactive goal state, tactic language, or general Lean elaborator. The fail-closed importer rejects declarations outside its supported profile.
Storage
Each fact has a typed statement, status, proof route, evidence references, assumptions, and provenance. The validator checks both the schema and semantic rules.
{
"id": "F:ml430-nat-fib-coprime-fib-succ-162fc738",
"epistemic_status": "proved",
"proof_route": "kernel-lean",
"axiom_footprint": [],
"external_status": "settled"
}Reuse
The graph connects facts to their dependencies and open descendants. After admission, Axeyum recomputes readiness from those edges. A new fact counts as cumulative progress when later reasoning can select it.