For most of its history, mathematics has been checked the way it was written: by people. A mathematician submits a proof, referees read it, and the field accepts a result once enough experts vouch for it. Lean replaces the referee with a machine. It is a programming language precise enough that a proof can be written out step by step and a computer can confirm each step, with no room for the gap a tired human reader might miss. Translating ordinary mathematics into that exact form is called formalization, and for years it was laborious enough to stay a curiosity. Then that curiosity started drawing in the field's most celebrated mathematicians, and close behind them the AI labs. The story of the last five years is how a proof checker became shared infrastructure, and why the people who built it now believe the same machinery is what AI-written software will need next.
Somewhere past two million lines, Mathlib stopped resembling anything mathematics had produced before. The community-built library of formalized mathematics, written in the Lean proof assistant, now spans undergraduate staples through research-frontier results, every line checked by machine rather than by referee. A 2024 Simons Institute workshop page put the count at one and a half million lines; the Lean site now says over two million. Comparable libraries took decades longer to reach similar scale: Mizar's library sits near 3.7 million lines and Isabelle's Archive of Formal Proofs near 4.8 million, each the accumulation of a generation of specialist labor.
