Every theorem in a proof assistant carries an exact, machine-readable list of the axioms its proof depends on. That makes a question measurable which usually stays qualitative in the foundations literature: what does an axiom cost? In other words: which part of the library do you lose if you drop it? This page collects the measurements done for the EEML programme, in a form that is useful to the proof-assistant community independently of EEML.
Lean/mathlib: axiom closure per theorem via Lean.collectAxioms over the full mathlib environment; random sample of 2,000 theorems out of 439,764 (seed 137), with binomial confidence intervals. The Diaconescu conflation (in Lean, choice also implies excluded middle) is resolved by recompiling proofs against an environment with classical logic but no witness extraction.
Coq/Rocq: full count rather than a sample. Lemma names harvested per module via Search is:Lemma, then the full closure per lemma via Print Assumptions (Coq 8.20.1, all non-compat modules; mathcomp 2.3.0). Primitive machine axioms (63-bit integers, floats) are counted separately and not booked as logical axioms.
Isabelle/HOL: full count over the distribution up to and including Complex_Main (Isabelle2025-2, session HOL-Proofs plus own audit sessions with record_proofs = 2): per named theorem the axiom closure via direct traversal of the proof terms, with memoisation over shared subproofs. Conventions: classical = True_or_False, choice = the someI/Eps axiom, infinity = the Suc_Rep axioms, extensionality reported separately; definitional axioms (typedef) not counted. Honest note: HOL has a classical kernel, so what is measured is "does the proof touch the axiom", exactly the same question as Lean's collectAxioms. The AFP sample uses the same setup: twelve random entries (seed 20260818, frame: session parent exactly HOL, 318 entries; build failure replaces per the frozen rule: 19 replacements, 17 of them build failures), each as its own proof-term session, counting only the entry's own theorems.
All scripts and seeds are archived; each measurement takes an evening to repeat. The setup runs without root privileges (packages unpacked locally).
| Corpus | Size | Logical axiom use | Detail |
|---|---|---|---|
| mathlib (Lean 4) | 439,764 theorems (sample 2,000) | ~93% uses something; choice 70.2% [68.2-72.3] | propext 90.5% · quotients 83.7% · genuine witness extraction ≤ 18.7% · classical-only ≥ 53.0% · constructive core 7.4% |
| Coq standard library 8.20.1 | 16,664 lemmas (full) | 11.5% | classical/LPO 11.0% · functional extensionality 10.5% (both almost entirely via the classical Dedekind reals) · genuine choice 0.03% · constructive 88.5% |
| mathcomp-analysis 1.9.0 (+ classical, reals) | 5,887 lemmas (full) | 77.2% | funext 77.1% · propext 77.1% · choice-like 69.2% · no LPO · the same community scores 0.0% on discrete work (frozen continuum test: hit) |
| Mathematical Components 2.3.0 | 11,442 lemmas (full) | 0.0% | ssreflect, finite groups, algebra: exactly zero axioms |
| Isabelle/HOL 2025-2 (distribution up to Complex_Main) | 30,340 theorems (full) | classical 88.1% · choice 44.1% | infinity 46.6% · extensionality 87.8% · discrete 93.7% vs continuum 92.1% (gradient 1.6 points: erased) · choice is a genuine choice in HOL |
| Archive of Formal Proofs 2026-08-26 (sample of 12 entries) | 5,655 theorems | classical 89.2% · choice 82.0% | infinity 81.9% · discrete 89.2% vs continuum 89.0% (gradient 0.2 points: erased) · choice saturates in contributed code, unlike in the distribution |
Prices are partly style, partly subject. Mathlib proves with global classical tactics and pays almost everywhere; mathcomp proves comparable discrete mathematics (up to and including the machinery behind the Odd Order theorem) with exactly zero axioms. Mathlib's 70.2% is therefore an upper bound within that proof style, not a property of mathematics itself. This conclusion was forced through a stake frozen in advance: the stake "prices are tool-independent" was measured and missed, and that miss is booked in the register.
What recurs in both ecosystems, since measured and hit as a frozen stake (13 August): axiom use concentrates where the continuum enters. The sharpest form is in the table: the same community, 0.0% on discrete work, 77.2% the moment the real numbers enter. In Coq nearly all axiom load sits with the real numbers; its discrete mathematics is axiom-free. In Lean the constructive core is 7.4% and the choice dependence sits in analysis and topology. Countable is cheap, the continuum is expensive.
The third measurement (18 August, expectations frozen in git beforehand): Isabelle/HOL confirms tool dominance at its sharpest. The discrete/continuum gradient, over 65 points in the Coq ecosystem, is fully erased in Isabelle: 93.7% versus 92.1%, a difference of 1.6 points, even slightly inverted. Once the tool saturates, the subject signal can no longer get through: that was frozen expectation V2, and it hit. Expectation V1 (classical-touch ≥ 90%) missed: it came out at 87.6% on the frozen corpus (88.1% on the extended one), and that miss is booked. The surprise sits with choice: where in Lean 70.2% hangs on the choice axiom, in Isabelle only 44.1% touches Hilbert choice: the classical logic does saturate there, the choice axiom does not. Three ecosystems, three profiles: the price table is definitively a property of the tool.
The AFP sample (same night, three expectations frozen in advance): V3 (classical-touch in the 85-95% band) hit at 89.2%. V4 (gradient < 20 points) hit convincingly: 0.2 points, even flatter than the distribution. V5 (choice remains a minority, < 60%) missed: user-contributed entries touch Hilbert choice in 82.0% of theorems, nearly double the distribution (44.1%). The lesson: the distribution core is built frugally, but contributed code leans almost entirely on the choice-bearing automation and library machinery. That miss, too, is booked.
For library maintainers (where does the axiom load sit, and is it needed?), for constructive mathematicians (which part of a corpus is already constructive without anyone calling it that?), and for anyone who prefers conducting foundations debates with numbers rather than intuitions. Natural extensions: the Archive of Formal Proofs (the Isabelle distribution itself is now measured), and a yearly remeasurement of mathlib (planned: August 2027, frozen prediction: 70.2% ± 5 points).
→ context: the Bayesian reading of axiom choice (mathematics page)