GONZALGO INDEXES
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.
The Kernel Index
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.
The Dominator Table
Mathlib constants ranked by how many theorems each is uniquely responsible for making classical — the number that would stop depending on the axiom of choice if that constant alone were rebuilt. Computed as a dominator tree over the reversed dependency graph rooted at the axiom.
What machine-generated Lean proofs rest on
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.
Using them
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.