Proof systems
Lean and the Axeyum kernel
Axeyum implements an independent Rust proof kernel for a selected Lean-core profile. Lean provides the reference language, elaborator, tactics, kernel, and package ecosystem.
Components
What is checked
- 2,586
- ledger facts admitted through the kernel
- 2,584
- kernel-route facts with an empty axiom footprint
- 7
- imported facts checked here and authored elsewhere python3 scripts/validate-facts.py @ 03ae4a3c9, 2026-10-05
The boundary
The checker consumes an exact export format and derives the type of each supported proof term. It does not parse Lean source, run tactics, or reproduce Lean's general elaborator.
The current profile targets selected constructs from Lean 4.30. Compatibility is a measured set of declarations, not a claim of full Lean compatibility.
Lean's own kernel replays that set. On 2026-09-10, Lean 4.34.0-rc1 accepted 4,394 of the 4,478 proved declarations
the Axeyum kernel builds. Lean refused 50 because their statements are
Type-valued and a Lean theorem must be a Prop; 34 more depend on one of those 50. No second kernel has confirmed
those 84 declarations.
Snapshot 03ae4a3c9 · 2026-10-05. Sources: PLAN.md § Status @ 03ae4a3c9; ADR-1661 (docs/research/09-decisions/adr-1661-the-replay-census-covers-every-carrier-and-type-valued-theorems-are-a-named-class.md), measured 2026-09-10; docs/internals/lean-kernel.md.