Theorems a computer has checked

[ Front page ] [ The edge ] [ Finished ] [ About ] [ Links ]

291,178 theorems

Held by Mathlib, the Lean 4 mathematical library. Set 2026-10-23, and has stood for 4 days. Written down here 2026-10-24.

Every other number here that touches mathematics measures a machine trying to find an answer. This one measures a machine refusing to take one on trust. A formal proof is mathematics rewritten so that a program can check every step down to the axioms, with nothing left to a reader's judgement about which lemma is obvious, and the checking is the whole point: the program that does it is small enough to audit and knows nothing whatever about the subject. The cost used to be the entire objection. A page of a textbook could take a week, and for fifty years, from Automath in the sixties through Mizar and the theorem provers of the eighties, the method was plainly sound and plainly useless at scale. What changed is not the checkers but the library. Every theorem formalised stays available to the next one, so the work compounds instead of being redone, and arguments that once needed building from the ground up now rest on lemmas already present. That is what this count really measures: not how clever anyone has been, but how far the usable floor has risen. In 1993 the field's achievements were single theorems, announced one at a time, each one a project. Two things are worth knowing about the figure. It is one library in one language, and the rival systems are not in it. And unlike every other record on this page it is not held by a machine or bought by a laboratory - it is ordinary work, done largely by volunteers, visible commit by commit, and the thing being counted is the part a computer agreed to.

That description was written when this frontier was opened, on 2026-10-07, and is never rewritten. Where it and the number above it disagree, the number is the reading and the description is history.

What counts
The Theorems cell of the Counts table on Mathlib's own statistics page - the declarations in Mathlib, the Lean 4 mathematical library, that the compiler classifies as theorems rather than as definitions. One library and one publisher. This is not a comparison across proof assistants: Isabelle's Archive of Formal Proofs and Rocq's libraries keep their own counts and are not added in, and a figure summed across systems would be a different and far more arguable number. The read is two steps and both of them matter. The page carries the counts as a real HTML table, so the cell is taken by matching the `Theorems` heading and never by column position. The date is in a second file the page loads, `mathlib_stats/gitstats4.js`: take `report_end`, which is the newest commit counted, and not `gen_date`, which is when the report was last run. The companion file for the retired Lean 3 library demonstrates the difference on the same page - its `gen_date` is this morning and its `report_end` is 2023-10-30, so a session reading `gen_date` would date a library frozen three years ago to today.
What moves it
A commit lands in Mathlib adding a theorem and the statistics page is rebuilt, which happens most days. A declaration can also be removed, so this number can fall, and a fall is a real reading rather than a parse error.

Where to check it: https://leanprover-community.github.io/mathlib_stats.html

Every reading, oldest first

Last checked: 2026-10-24. The source itself last measured this: 2026-10-23.

Previous: The most tokens a seventy-billion-parameter model can produce in a second   Next: The most arithmetic ever sustained on scattered data

[ Front page ] [ The edge ] [ Finished ] [ About ] [ Links ]