THE KERNEL INDEX
what formal libraries actually rest on
Each library here was measured directly. The two middle columns are the ones to read: how many theorems rest on a proof that was never finished, and how many were settled by running compiled code rather than by the kernel.
Measured with gonzalgo · Lean 4.32.1 with Mathlib · Metamath set.mm, iset.mm, nf.mm, ql.mm, hol.mm
| library | system | foundation | theorems | unfinished | compiler-trusted | optional axiom |
|---|---|---|---|---|---|---|
| Mathlib | Lean 4 | Dependent type theory | 437,429 | 0 | 0 | 66.62% |
| Lean core (Init) | Lean 4 | Dependent type theory | 45,051 | 0 | 0 | 23.91% |
| Std | Lean 4 | Dependent type theory | 34,510 | 0 | 0 | 56.66% |
| Lean core (Lean) | Lean 4 | Dependent type theory | 9,281 | 0 | 0 | 12.83% |
| Batteries | Lean 4 | Dependent type theory | 5,249 | 0 | 0 | 32.63% |
| Aesop | Lean 4 | Dependent type theory | 771 | 0 | 0 | 12.97% |
| ProofWidgets | Lean 4 | Dependent type theory | 165 | 0 | 0 | 27.88% |
| Plausible | Lean 4 | Dependent type theory | 87 | 0 | 0 | 6.9% |
| Lean 4 | Dependent type theory | 36 | 0 | 0 | 19.44% | |
| set.mm | Metamath | ZFC set theory, classical first-order logic | 47,621 | 0 | — | 1.22% |
| iset.mm | Metamath | Intuitionistic set theory | 16,236 | 0 | — | — |
| nf.mm | Metamath | Quine's New Foundations | 5,976 | 0 | — | — |
| ql.mm | Metamath | Quantum logic | 1,140 | 0 | — | — |
| hol.mm | Metamath | Higher-order logic | 151 | 0 | — | — |
Red marks a non-zero count — theorems resting on an unfinished proof, or on the compiler. unfinished counts theorems reaching a sorry (Lean) or a ?-bearing proof (Metamath) anywhere upstream, not only those that state one. optional axiom is the share of theorems depending on Classical.choice in Lean and on full choice in set.mm; the other databases declare no choice axiom.
Get the data
kernel-index.json · kernel-index.csv · CC-BY-4.0 · version 2026-08-05
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
pip install gonzalgo gonzalgo trust mathlib_split.tsv # the Lean rows gonzalgo mm set.mm iset.mm nf.mm ql.mm hol.mm # the Metamath rows
Every figure comes from the proof system's own bookkeeping — Lean's collectAxioms and Metamath's proof structure. The extractors ship with the tool, so you can re-derive any row here yourself.
Why it exists
“This library rests on nothing but the kernel” is something people have had to take on faith, because checking it at library scale wasn't practical. The numbers above are that check. A zero in the middle columns means someone ran it and it came back empty.