THE MODULE SPEND TABLE

which files spend the axiom, and on which primitive

A library-wide figure names no file. 18,109 declarations across 3,261 of Mathlib's 10,599 modules name a choice primitive in their own proof, and this is where they are.

Only 209 of those cite Classical.choice itself. 9,442 go through Classical.byContradiction and 8,440 through Classical.propDecidable — excluded middle and the decidability fallback. A repair aimed at one does nothing for the others, which is why they are counted apart.

Measured with gonzalgo · Lean 4.33.0 with Mathlib v4.33.0 · one streamed pass over 795,218 declarations, no closure computed

module	library	declarations	spends	rate	byContradiction	propDecidable	choice
Batteries.Data.List.Lemmas	Batteries	881	168	19.1%	166	2	0
Mathlib.Topology.EMetricSpace.BoundedVariation	Mathlib	268	108	40.3%	104	2	0
Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence	Mathlib	291	85	29.2%	85	0	0
Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter	Mathlib	251	85	33.9%	85	0	0
Mathlib.Algebra.BigOperators.Group.Finset.Basic	Mathlib	373	79	21.2%	41	46	0
Mathlib.MeasureTheory.VectorMeasure.Basic	Mathlib	331	69	20.8%	3	67	0
Mathlib.Algebra.Homology.SpectralObject.SpectralSequence	Mathlib	290	64	22.1%	56	8	0
Mathlib.Data.Finset.Card	Mathlib	264	63	23.9%	50	15	0
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	Mathlib	257	62	24.1%	0	62	0
Mathlib.RingTheory.Polynomial.Resultant.Basic	Mathlib	235	59	25.1%	51	6	0
Mathlib.Logic.Basic	Mathlib	365	58	15.9%	16	39	1
Mathlib.Algebra.BigOperators.Finprod	Mathlib	352	57	16.2%	14	43	0
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms	Mathlib	213	57	26.8%	57	0	0
Mathlib.Topology.Sets.VietorisTopology	Mathlib	322	57	17.7%	51	3	0
Mathlib.GroupTheory.Nilpotent	Mathlib	432	54	12.5%	18	34	0
Mathlib.RingTheory.MvPolynomial.MonomialOrder	Mathlib	232	54	23.3%	5	47	0
Mathlib.Analysis.SumIntegralComparisons	Mathlib	85	53	62.4%	53	0	0
Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult	Std	237	53	22.4%	53	0	0
Mathlib.Data.Finset.Basic	Mathlib	244	52	21.3%	49	5	0
Mathlib.CategoryTheory.Limits.Shapes.Biproducts	Mathlib	411	50	12.2%	0	49	1
Mathlib.Combinatorics.SimpleGraph.Paths	Mathlib	392	50	12.8%	46	7	0
Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas	Std	238	50	21.0%	49	1	0
Mathlib.Algebra.Homology.Factorizations.CM5a	Mathlib	201	49	24.4%	48	0	0
Mathlib.Data.List.Sort	Mathlib	336	48	14.3%	47	1	0
Mathlib.Data.Finsupp.Single	Mathlib	154	47	30.5%	34	37	0
Mathlib.Order.Interval.Set.LinearOrder	Mathlib	217	46	21.2%	46	0	0
Mathlib.Data.Set.Image	Mathlib	464	45	9.7%	44	1	0
Init.Data.BitVec.Lemmas	Init	2,051	44	2.1%	3	41	0
Mathlib.Data.List.Basic	Mathlib	484	44	9.1%	43	1	0
Mathlib.Data.Set.Insert	Mathlib	203	44	21.7%	44	0	0
Mathlib.LinearAlgebra.AffineSpace.Combination	Mathlib	127	44	34.6%	0	12	32
Mathlib.Order.ConditionallyCompleteLattice.Basic	Mathlib	279	44	15.8%	4	40	0
Mathlib.Data.Set.Prod	Mathlib	384	42	10.9%	38	4	0
Mathlib.NumberTheory.Chebyshev	Mathlib	266	42	15.8%	42	1	0
Mathlib.Data.List.Chain	Mathlib	215	41	19.1%	41	0	0
Mathlib.AlgebraicTopology.ExtraDegeneracy	Mathlib	171	40	23.4%	40	0	0
Mathlib.Combinatorics.SimpleGraph.Acyclic	Mathlib	179	40	22.3%	28	14	0
Mathlib.Probability.Process.HittingTime	Mathlib	102	40	39.2%	11	32	0
Mathlib.Algebra.Polynomial.RuleOfSigns	Mathlib	70	39	55.7%	37	0	0
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation	Mathlib	109	39	35.8%	39	0	0
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne	Mathlib	160	38	23.8%	0	38	0
Mathlib.Algebra.Homology.HomotopyCategory.MappingCone	Mathlib	201	37	18.4%	37	0	0
Mathlib.Analysis.SpecialFunctions.Artanh	Mathlib	81	37	45.7%	37	2	0
Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema	Mathlib	76	37	48.7%	31	0	0
Mathlib.NumberTheory.Modular	Mathlib	173	37	21.4%	34	1	0
Mathlib.NumberTheory.Padics.PadicNumbers	Mathlib	312	37	11.9%	2	37	0
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift	Mathlib	186	36	19.4%	36	0	0
Mathlib.MeasureTheory.Function.SimpleFunc	Mathlib	497	36	7.2%	2	35	1
Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE	Mathlib	237	35	14.8%	35	0	0
Mathlib.Order.SuccPred.Basic	Mathlib	408	35	8.6%	4	31	0
Batteries.Data.Fin.Lemmas	Batteries	180	34	18.9%	34	0	0
Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone	Mathlib	135	34	25.2%	34	0	0
Mathlib.Algebra.Homology.TotalComplexShift	Mathlib	100	34	34.0%	34	0	0
Mathlib.MeasureTheory.Integral.SetToL1	Mathlib	184	34	18.5%	0	34	0
Mathlib.Order.SuccPred.Limit	Mathlib	295	34	11.5%	2	30	0
Init.Classical	Init	67	33	49.3%	0	20	5
Mathlib.Algebra.Ring.Int.Parity	Mathlib	96	33	34.4%	33	0	0
Mathlib.Order.RelSeries	Mathlib	382	33	8.6%	31	0	0
Mathlib.Algebra.Homology.HomotopyCategory.HomComplex	Mathlib	316	32	10.1%	32	0	0
Mathlib.Analysis.Analytic.Order	Mathlib	133	32	24.1%	16	16	0
Mathlib.Data.List.Lattice	Mathlib	112	32	28.6%	32	0	0
Mathlib.Analysis.BoxIntegral.Partition.Basic	Mathlib	221	31	14.0%	0	31	0
Mathlib.Algebra.Polynomial.Roots	Mathlib	210	30	14.3%	5	25	0
Mathlib.Algebra.Ring.Parity	Mathlib	186	30	16.1%	30	0	0
Mathlib.CategoryTheory.GlueData	Mathlib	172	30	17.4%	0	30	0
Mathlib.CategoryTheory.NatIso	Mathlib	152	30	19.7%	30	0	0
Mathlib.Data.Finset.Insert	Mathlib	260	30	11.5%	30	0	0
Mathlib.Data.List.Cycle	Mathlib	442	30	6.8%	30	0	0
Mathlib.CategoryTheory.Functor.Category	Mathlib	118	29	24.6%	29	0	0
Mathlib.Data.Finsupp.Basic	Mathlib	373	29	7.8%	7	23	0
Mathlib.RingTheory.HahnSeries.Basic	Mathlib	185	29	15.7%	0	29	0
Mathlib.Topology.FiberBundle.Trivialization	Mathlib	355	29	8.2%	0	29	0
Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter	Mathlib	123	28	22.8%	28	0	0
Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality	Mathlib	50	28	56.0%	22	6	0
Mathlib.GroupTheory.OrderOfElement	Mathlib	575	28	4.9%	4	18	0
Mathlib.GroupTheory.Perm.Fin	Mathlib	122	28	23.0%	28	0	0
Mathlib.Logic.Function.Basic	Mathlib	360	28	7.8%	9	18	4
Init.Data.Char.Ordinal	Init	91	27	29.7%	27	0	0
Mathlib.Algebra.MvPolynomial.Degrees	Mathlib	122	27	22.1%	3	24	0
Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic	Mathlib	188	27	14.4%	27	0	0
Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic	Mathlib	69	27	39.1%	2	25	0
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic	Mathlib	275	27	9.8%	21	6	0
Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph	Mathlib	238	27	11.3%	26	1	0
Mathlib.Data.DFinsupp.Defs	Mathlib	358	27	7.5%	23	3	0
Mathlib.FieldTheory.RatFunc.Basic	Mathlib	324	27	8.3%	0	27	0
Mathlib.Logic.Equiv.Defs	Mathlib	405	27	6.7%	24	3	0
Mathlib.Order.KrullDimension	Mathlib	252	27	10.7%	21	1	0
Mathlib.Algebra.Homology.HomotopyCategory.KInjective	Mathlib	56	26	46.4%	26	0	0
Mathlib.Data.Option.NAry	Mathlib	61	26	42.6%	26	0	0
Mathlib.Geometry.Manifold.IsManifold.Basic	Mathlib	261	26	10.0%	4	22	0
Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas	Mathlib	71	26	36.6%	23	4	0
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody	Mathlib	109	26	23.9%	0	26	0
Mathlib.Order.SupIndep	Mathlib	114	26	22.8%	16	18	0
Mathlib.Analysis.Meromorphic.NormalForm	Mathlib	114	25	21.9%	4	22	0
Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass	Mathlib	260	25	9.6%	5	21	0
Mathlib.Data.Finset.Prod	Mathlib	140	25	17.9%	24	2	0
Mathlib.Data.Int.Init	Mathlib	148	25	16.9%	25	0	0
Mathlib.Data.List.PeriodicityLemma	Mathlib	46	25	54.3%	25	0	0
Mathlib.Data.List.Sigma	Mathlib	243	25	10.3%	25	0	0
Mathlib.Data.Nat.Log	Mathlib	152	25	16.4%	25	0	0
Mathlib.Logic.Equiv.Basic	Mathlib	356	25	7.0%	24	1	0
Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic	Mathlib	56	25	44.6%	1	25	0
Mathlib.RingTheory.DedekindDomain.Factorization	Mathlib	127	25	19.7%	2	22	0
Init.Data.Nat.Lemmas	Init	768	24	3.1%	0	24	0
Mathlib.Algebra.Homology.Embedding.TruncGE	Mathlib	86	24	27.9%	0	24	0
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital	Mathlib	529	24	4.5%	0	24	0
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle	Mathlib	317	24	7.6%	24	0	0
Mathlib.Computability.TuringMachine.PostTuringMachine	Mathlib	457	24	5.3%	8	21	0
Mathlib.Data.Fin.SuccPred	Mathlib	290	24	8.3%	24	0	0
Mathlib.Data.Set.Sigma	Mathlib	102	24	23.5%	23	1	0
Mathlib.GroupTheory.Exponent	Mathlib	169	24	14.2%	4	20	0
Mathlib.LinearAlgebra.RootSystem.Chain	Mathlib	79	24	30.4%	9	15	0
Mathlib.Order.Interval.Finset.Gaps	Mathlib	68	24	35.3%	20	0	0
Mathlib.Probability.Distributions.Uniform	Mathlib	67	24	35.8%	1	23	0
Mathlib.Topology.Covering.Basic	Mathlib	163	24	14.7%	0	24	0
Std.Data.DTreeMap.Internal.Balancing	Std	368	24	6.5%	1	23	0
Mathlib.AlgebraicTopology.DoldKan.Faces	Mathlib	45	23	51.1%	23	0	0
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital	Mathlib	556	23	4.1%	1	22	0
Mathlib.Data.Set.Card	Mathlib	445	23	5.2%	13	10	0
Mathlib.MeasureTheory.VectorMeasure.SetIntegral	Mathlib	104	23	22.1%	9	15	0

Showing the first 120 of 3,261 rows. Ordered by spends. The tail is long: most spending modules do it once or twice. The full set is in the JSON and the CSV.

spends counts declarations in the module whose own proof names a primitive; a declaration naming two is counted once here and once under each primitive, so the primitive columns can exceed it. rate is spends over declarations in that module. Modules with no direct spend are omitted — there are 7,338 of them, and their theorems can still depend on choice through imports.

Get the data

module-spend.json · module-spend.csv · CC-BY-4.0 · version 2026-08-13

One of the gonzalgo indexes — standing measurements of what formal libraries rest on, remeasured as the libraries move. Cite the series as 10.5281/zenodo.21900625, which resolves to the current deposit.

Reproduce it

lake env lean -D maxErrors=4000 Split.lean
python extract_module_spend.py

One pass, about seven seconds over a 640 MB dump. The module column comes from the extractor; a dump without it cannot answer this question at all. Method: 10.5281/zenodo.21769846.

Spending is not reach

This table answers where the axiom is used. It does not say how far each use travels, and the two are wildly different: 324,808 theorems depend on choice while 18,109 declarations spend it. One spend in Mathlib.Logic.Basic can be inherited by a hundred thousand theorems, and one in a leaf file by none.

The Dominator Table is the other half — how many theorems each site is responsible for. Read together they say which file to open and whether opening it is worth anything.

What the primitives mean

Classical.byContradiction is excluded middle: proving P by refuting its negation. Classical.propDecidable is the decidability fallback, supplied where an instance was wanted and none was synthesised. Classical.choice proper is choosing from a family, and is the rarest of the three by two orders of magnitude.

That ordering matters for anyone trying to reduce classical dependence. The common cases are not choice in the mathematician's sense at all — they are a proof style and a missing instance.

Where it concentrates

The heaviest single module is Batteries.Data.List.Lemmas at 168 spends across 881 declarations. By library the split is Mathlib 3,099, Init 99, Std 38, Batteries 20, Lean 3, Plausible 2 modules containing at least one spend.