Every theorem in a proof library rests on a measurable set of axioms, and a library’s distribution of those sets — its axiom profile — is a fact about the mathematics, not an opinion about it. This paper measures the profile of the entire Mathlib library: 707,053 declarations at a pinned commit, each declaration’s transitive axiom closure computed from a content-addressed archive of the elaborated terms, certified against the Lean kernel by full replay. The findings: 25.09% of Mathlib (177,395 declarations) depends on no axioms at all; only 23 distinct axiom profiles occur in the whole corpus, and 99.96% of declarations lie on the Boolean cube over three axioms — propositional extensionality, quotient soundness, and choice; the library contains zero incomplete proofs. Choice reaches half the corpus (50.84%), but its entry structure is extraordinarily narrow: every choice-dependent declaration reaches the axiom through a frontier of just 206 declarations that use it directly, and a structural counterfactual over the dependency graph shows 55.4% of all choice-dependence flowing through three generic classical-instance gateways jointly. The measurement separates two things the per-declaration view conflates: mathematics that needs choice, and mathematics that inherits choice from shared infrastructure. Every figure is recomputable from the query outputs deposited with this paper.
Larsen James Close (Tue,) studied this question.