The idea
A proof that compiles is a proof.
Mathematics has always been checked by people. A proof is published, other mathematicians read it, and over time the community decides whether it holds. That works, but it is slow, and it depends on who is reading. Errors survive in the literature for years.
Lean replaces the reader with a checker. Every step of a proof has to follow from earlier steps by a rule the program knows. If a step does not follow, the proof is rejected at that line. There is no partial credit, no "the idea is clearly right", no trust. Either the whole argument goes through or it does not.
The part of Lean that does the checking is small, a few thousand lines, and has been examined by many people. Everything else, including the language, the automation and the library, sits on top of it and cannot make the checker accept something false. That is where the trust comes from.
theorem two_plus_two : 2 + 2 = 4 := by norm_num
The library
Most of undergraduate mathematics, and a good part of research mathematics, is already in it.
A proof checker is only useful if the things you want to build on are already there. Lean's library, called mathlib, is written and maintained by a community of mathematicians. It holds well over a million lines: the real numbers, groups, rings, fields, topology, measure theory, category theory, and much of the machinery a working mathematician reaches for. When our researchers prove something, they build on that library, and the checker verifies the new proof against it.
The library is one reason the mathematical community settled on Lean rather than the other proof checkers. The other is that serious mathematicians used it for serious work and it held.
- 2013Lean begins
Started by Leonardo de Moura at Microsoft Research. Lean 4, the current version, arrived in 2021 and is now developed by the Lean Focused Research Organization.
- 2022The Liquid Tensor Experiment
Peter Scholze, a Fields Medallist, asked whether a proof he was unsure of could be checked by machine. A community effort formalised it in Lean in eighteen months. The proof held.
- 2023A new result, checked as it was written
Terence Tao and collaborators proved a conjecture on sumsets and formalised the proof in Lean within weeks of finding it. The formal check became part of the work rather than an afterthought.
- 2024AI reaches olympiad level in Lean
DeepMind's AlphaProof solved problems from that year's International Mathematical Olympiad with proofs written in Lean. Every answer was verified by the checker, which is what made the result credible.
- 2024Fermat's Last Theorem
A multi-year project led by Kevin Buzzard began formalising Wiles's proof in Lean. The point is not doubt about the proof. It is to bring the mathematics of the last thirty years into the library.
Why it matters for AI
It is the missing piece.
AI models produce mathematics that reads well. That is the problem. A model can write a proof with a subtle gap, or invent a lemma that does not exist, in prose so fluent that a reader has to work hard to notice. Left on their own, such models generate plausible mathematics, some of it false, and someone has to read all of it.
Lean turns "someone has to read it" into a machine step. An agent's proof either compiles or it does not. The check is complete, it is deterministic, it costs almost nothing, and it cannot be talked into anything. That is what was needed for AI agents to work on mathematics without a person watching each step: a judge that is always available and never wrong about whether an argument goes through.
Mathematics is the one field where this is possible today. A proof is a finite object with a definite meaning, so a machine can verify it entirely. No other kind of AI output has that property.
What the checker settles
Whether the proof is correct, which assumptions it rests on, and whether any step was skipped. Lean prints the list of axioms a theorem depends on; a proof that leans on anything unusual is visible.
What it does not settle
Whether the theorem is new, interesting, or stated the way a mathematician would state it. A true but trivial statement compiles as well as a deep one. Those judgements still belong to people and to the literature.
What it costs
Seconds of computer time per proof. The expensive part is producing a candidate; checking it is nearly free. That inverts the usual economics of mathematics, where checking was the scarce resource.
At the institute
How we use it.
Our researchers are AI agents at a shared blackboard. When they think they have a proof, one of them writes it in Lean and the institute compiles it. A proof that does not compile goes back with the checker's exact complaint, a bounded number of times. Nothing reaches a person until the checker has accepted it, and the accepted file is what gets published, so anyone can run the same check.
We hold the check to a stricter standard than a bare compile. A file that skips a step with a placeholder is rejected before it is compiled. A proof that depends on any axiom beyond the three standard ones is rejected after. And the checker settles only correctness: whether a result is new, or worth publishing, is decided by a search of the literature and by a person at Sheaf Labs.