Where Formal Libraries Spend Their Axioms: A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's omega
Abstract
A proof assistant can report which axioms a theorem rests on, but only one theorem at a time, and only whether rather than why. I measure axiom use across six libraries and two proof systems - the Metamath databases set.mm (ZFC, classical first-order), iset.mm (intuitionistic), nf.mm (Quine's New Foundations), ql.mm (quantum logic) and hol.mm (higher-order logic), and Lean 4's Mathlib (dependent type theory) - using one program for all six, so the comparison rests on identical definitions rather than analogy.
Axiom use funnels through very few lemmas in the mature libraries. The median axiom is cited directly in 2 to 4 proofs and inherited by thousands, and entry points per theorem agree to within 13% across set.mm, iset.mm and nf.mm despite three different foundations. Two smaller databases, ql.mm and hol.mm, sit three to six times higher, so the concentration is a property of maturity rather than of formal libraries as such - a narrowing of what version 1.0.0 of this paper claimed. The mechanism is ordinary: a young library has not yet had its shared subproofs factored out into gateway lemmas.
A refactoring-invariance result settles which of these measurements can bear comparison between libraries. Under inlining and factoring - operations that change how a library is written, not what it proves - the dependent set is invariant while the entry-point set is not, so amplification can be driven to any value between 1 and the number of dependents. No bound on amplification can therefore depend on mathematical content alone. Reach is invariant, and is the quantity reported: full choice in set.mm reaches 1.2% of the library against Classical.choice's 61.0% of Mathlib.
Separating each theorem's statement from its proof bounds how much classical dependence is even eligible for removal: 13.1% of Mathlib theorems have a choice-free statement and a choice-dependent proof, and nothing outside that band can be eliminated under any argument.
A substitutability test re-synthesizes each site where the elaborator inserted classical decidability and classifies the result by the kernel's own axiom bookkeeping rather than by name - a name-based screen on set.mm measured 41.5% precision, its characteristic failure being a lemma that relocates choice into an antecedent instead of discharging it. Across 8,907 declarations and 23,279 verdicts the test finds 805 sites where a choice-free instance was available and unused, and 280 declarations whose only route to Classical.choice runs through such a site.
Those 280 share a cause. 276 of them (98.6%) trace to the omega decision procedure, which supplies the Decidable arguments of six helper lemmas as a literal Classical.propDecidable and never attempts instance synthesis. On Nat and Int, where the required instances exist and are axiom-free, this makes otherwise constructive proofs depend on the axiom of choice. It reproduces in one line with no imports, and the hardcoded instances are still present in Lean master as of August 2026.
The fix is applied rather than only proposed, and then tested for whether it preserves the proofs. Rewriting all 280 proof terms and submitting each to the kernel against its unchanged statement, 276 are accepted and 4 are rejected, and the four rejections are exactly the four declarations traced to a cause other than omega. 275 declarations lose their dependence on Classical.choice outright. The partition is structural: omega passes the instance to a helper lemma and never computes with it, so its terms are indifferent to which instance they receive, while the four exceptions use decidability computationally and break.
Reported upstream, the issue was closed as completed with the reply that avoiding choice is a deliberate non-goal of Lean core. No figure was disputed. The behaviour is therefore within Lean's stated design rather than a defect by its own standard, and the reply also serves as a primary source for the paper's reading of why set.mm and Mathlib differ so widely in reach - set.mm tiers countable and dependent choice separately on purpose, and Lean core does not.
The paper also documents a measurement hazard specific to Lean 4.32: ConstantInfo.value? returns none for theorems unless called with allowOpaque := true, so an extractor written the obvious way sees no proof terms, silently measures statements, and reports them as proofs. This invalidated a full round of results before an exact zero in a 2x2 classification exposed it. The superseded data is included so the error remains checkable.
Code, all 23,279 verdicts, the 280 declarations and the per-declaration kernel outcomes are included. A single command recomputes every quantitative claim from the shipped artifacts and reports OK or MISMATCH against the published value.
The measurement pipeline is packaged as gonzalgo (pip install gonzalgo), and the standing survey it produces - what 14 formal libraries across 2 proof systems rest on - is published as the Kernel Index at https://www.f-keys.com/gonzalgo/kernel-index/
Changes in 1.0.2: the cross-foundation comparison gains ql.mm and hol.mm, which narrow the concentration claim from formal libraries generally to mature ones; a new section records the upstream outcome and corrects an over-reading of an earlier accepted Lean issue as general policy; the abstract's library count is corrected to six.
Cite it
Gonzalez, V. (2026). Where Formal Libraries Spend Their Axioms: A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's omega. Zenodo. https://doi.org/10.5281/zenodo.21769846