measurements, kept current, in a form you can download
What a formal library rests on is a fact about it that changes when the library changes. These are the measurements taken so far, each with the table on the page and the same table as JSON and CSV.
Every figure comes from the proof system's own bookkeeping — Lean's
collectAxioms and Metamath's proof structure — read by
gonzalgo, which proves nothing itself. Each index says
which version of which library it was taken from, and carries a version that
moves only when the numbers do.
What formal mathematical libraries rest on: theorems depending on an unfinished proof, on the compiler rather than the kernel, and on an optional axiom. Measured by one program across two proof systems and six foundations.
Sites of classical dependence in Mathlib ranked by how many theorems each is uniquely responsible for — the number that would stop depending on the axiom of choice if that site alone were rebuilt. Computed as a dominator tree over the reversed dependency graph rooted at the axiom, with chains of constants that free the same theorems collapsed to a single site.
A controlled experiment over Lean tactics. 27 arithmetic goals over Nat and Int, each put to ten tactics, with the axiom set recorded for every cell. Holding the goal fixed and varying only the tactic separates a classical dependence introduced by the proof from one required by the statement.
The 20 largest sites of classical dependence in Mathlib, each with the number of declarations in its dominator subtree that cite a choice primitive directly. Separates sites where the axiom is spent from sites that dominate theorems while inheriting the axiom from further up.
Kernel-verified substitution attempted against the 20 largest sites of classical dependence in Mathlib. For each declaration: occurrences of Classical.propDecidable in its proof term, how many the harness could reach, how many had a Decidable instance synthesised, and how many produced a term the kernel accepted.
Axioms used, direct entry points into them, and entry points per theorem, for five Metamath databases spanning five foundations. Entry points per theorem normalises for library size and is the measure that can be compared across databases; amplification is carried as reported but is a property of factorization rather than of mathematics.
Rates at which Lean tactics' proofs carry an avoidable classical dependence, across four libraries under two attribution rules, each shown against the band spanned by known-negative tactics in the same library and rule. The band is what makes a rate interpretable, and it is wide.
Declarations in Lean 4 core, Std, Batteries, Mathlib and Plausible where a rewrite removing a classical dependence was attempted, with the module, the compiler-generated proof term carrying the dependence, the outcome, and the kernel's reason where it refused.
Every $a statement in Metamath's set.mm — logical axioms, definitions and syntax constructors kept apart — with the number of the library's 47,621 theorems whose proof closure reaches it, and that count as a share of the library.
Sites of classical dependence in Lean 4 examined for constructive replacement and not removed, each with the reason: no instance could be synthesised, the occurrence was not in a position where an instance is supplied, the available instance itself depends on choice, or synthesis timed out.
The 1,528 theorems in Metamath's set.mm whose proofs reach a choice principle, each labelled with the strongest of the three the database declares separately — full choice, countable choice, dependent choice — together with the raw membership in all three.
Declaration-graph differences between two Mathlib releases, measured by the same extractor on both sides. Separates declarations added and removed from those that kept their name — and among those, separates a changed statement from a changed proof.
Modules containing at least one declaration whose own proof term names a choice primitive directly, with the count broken down by primitive. Spending, as opposed to reach: a module with no direct spend can still be full of theorems that depend on choice through what they import.
Every $a statement across five Metamath databases spanning five foundations, with the number of that database's theorems whose proof closure reaches it and the number citing it directly. Assertions are separated from well-formedness constructors by typecode.
What a corpus of machine-generated Lean 4 proofs rests on. 9,169 Goedel-Prover proofs of Lean Workbook problems that compile under Lean 4.32, audited for unfinished proofs, compiler-trusted reductions and axiom dependence, with choice dependence split into the part the statement forces and the part the proof adds.
CC-BY-4.0: use them, quote them, redistribute them, cite the DOI on the index you used. If a number here disagrees with one you measured, that is worth an issue — the point of publishing the data is that someone can check it.