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,343
- ledger facts admitted through the kernel
- 2,341
- kernel-route facts with an empty axiom footprint
- 7
- imported facts checked here and authored elsewhere python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03
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.
Snapshot a103b3db3 · 2026-09-03. Sources: docs/PROJECT-STATE.md § Evidence and Lean @ a103b3db3, measured 2026-08-21; docs/internals/lean-kernel.md.