Where Formal Libraries Spend Their Axioms: A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's omega

Abstract

A proof assistant reports which axioms a theorem rests on one theorem at a time, and only whether rather than why. I measure axiom use across four libraries and two foundations - the Metamath databases set.mm (ZFC, classical first-order), iset.mm (intuitionistic) and nf.mm (Quine's New Foundations), and Lean 4's Mathlib (dependent type theory) - using one program for all four, so the comparison rests on identical definitions rather than analogy. Axiom use funnels through very few lemmas in every library measured. The median axiom is cited directly in 2 to 4 proofs and inherited by thousands: overall amplification is 292x, 221x and 94x in the three Metamath databases, and 2,256x for Classical.choice in Mathlib, whose 144 entry points among 532,605 theorems reach 324,808 of them. 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, a design difference, since set.mm tiers countable and dependent choice separately on purpose. 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 with no imports: "theorem t (a b : Nat) : a - b = 0 <-> a <= b := by omega" rests on Classical.choice, while splitting the connective by hand and giving omega the same work on each side does not. 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. 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.