Formal libraries
mathlib and the Axeyum fact ledger
Axeyum implements a typed formal library and fact ledger for several proof and computation routes. mathlib is the principal reference library for Lean and is much larger.
Components
Current ledger
- 2,714
- fact records checked by the validator
- 2,425
- distinct propositions established
- 262
- open facts python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03
Classical and constructive foundations
mathlib supports both constructive and classical mathematics. Its axiom footprint therefore belongs to each declaration, not to the library as a whole. Lean can report that footprint.
Axeyum
The constructed base has no axioms
Axeyum constructs logic, natural numbers, integers, rational numbers, strings,
constructive real and complex numbers, and constructive points inside its kernel. The
current inventory reports a trusted surface of zero for all 8
packages. None uses propext, Classical.choice, or
Quot.sound.
mathlib
Classical analysis can depend on three axioms
At the pinned mathlib commit, the standard intermediate value and compact-extremum
declarations listed below each depend on propext,
Classical.choice, and Quot.sound. Other mathlib declarations
have smaller or empty footprints.
Measured mathlib analysis declarations
| Declaration | Axiom footprint |
|---|---|
intermediate_value_Icc | propext, Classical.choice, Quot.sound |
intermediate_value_Icc' | propext, Classical.choice, Quot.sound |
IsCompact.exists_isMaxOn | propext, Classical.choice, Quot.sound |
IsCompact.exists_isMinOn | propext, Classical.choice, Quot.sound |
One integer goal across four routes
| Route | Axiom footprint |
|---|---|
| General ordered-ring proof | none |
| Axeyum constructed Int | none |
| Lean standard Int | propext |
| Lean omega on the same goal | propext, Quot.sound |
Snapshot a103b3db3 · 2026-09-03. Sources: python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03; nat_axiom_inventory @ a103b3db3, 2026-09-03; docs/mathematics-2026-08/01-decide-vs-certify.md and ADR-0875 @ a103b3db3. mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f; Lean 4.30.0.