Lean, formalization, and why proof-checking changes the game more than proof-finding

Most of the news about AI and math is about finding proofs. A model solves olympiad problems, a model gets a gold medal, a model proves a lemma a human was stuck on. Those results are real and I find them exciting. But I think the more important story is happening one step later, in the part where somebody checks whether the proof is right.

A formal checker offers something I want from AI mathematics: a way to reject an invalid derivation even when it reads convincingly. Lean and four formalization projects helped me understand both that promise and the work it takes to get there.

What Lean and Mathlib actually are

Lean is a programming language that doubles as a proof assistant.¹ You write a mathematical statement in it, the same way you’d write a function signature, and then you write a proof, which is a program that Lean can check. Lean checks whether the submitted proof establishes the formal statement under its declared axioms. A valid informal proof may still need substantial work before Lean accepts its formal version, and Terence Tao described what that looks like on screen in a 2023 tour: “all the squiggly underlines have disappeared, indicating that Lean has accepted this as a valid proof.”²

The part that does the accepting is small. The Equational Theories Project’s write-up (more on that project below) gives a clear account of how Lean is built. There’s a kernel, which checks proofs written in a very spare core logic. On top of it sits an elaborate language with “tactics,” automated helpers that search libraries, simplify expressions, and fill in routine steps. Whatever the tactics produce gets translated down into the core logic, and the kernel checks that. The kernel is described there as “the smallest and most trusted piece.”¹ So you don’t have to trust the clever automation. You only have to trust the small checker at the bottom.

Mathlib is the library that makes Lean useful for real math. A 2019 paper from the mathlib Community describes it as “a community-driven effort to build a unified library of mathematics.”³ It’s where definitions like groups, topological spaces, measures, and so on live, along with the theorems about them. If you want to formalize a new result, you’re almost always building on top of Mathlib, and if the definitions you need aren’t there, you have to add them first. That last point turns out to be the main cost of the whole enterprise, and I’ll come back to it.

For calibration: I’ve done small Lean exercises, the kind where you prove facts about natural numbers, and I have never contributed anything to Mathlib. So treat what follows as a careful reader’s view, not a practitioner’s.

The Liquid Tensor Experiment

The project that made a lot of research mathematicians take Lean seriously started with a blog post. In December 2020, Peter Scholze wrote a guest post on Kevin Buzzard’s Xena blog challenging people to formalize a theorem he’d proved with Dustin Clausen about “liquid vector spaces.”⁴

His reasons were unusually candid. He wrote “I think this may be my most important theorem to date,” and also that “being 99.9% sure is not enough.”⁴ The proof was hard, it was technical, and in his words “nobody else has dared to look at the details of this, and so I still have some small lingering doubts.”⁴ This wasn’t a famous old theorem being formalized as a showcase. It was a working mathematician asking a machine to check something he wasn’t sure about himself.

Six months later, in June 2021, he wrote a follow-up. The team had formalized the part of the argument he was worried about, and he wrote that he had “no remaining doubts about the correctness of the main proof.”⁵ He also said he found it “absolutely insane that interactive proof assistants are now at the level” where this was possible.⁵

The part of that follow-up I find most interesting is a different admission. He wrote that when he posed the challenge, “I did not understand why the argument worked.”⁵ Formalizing it forced the argument into pieces small enough that he could see what was actually doing the work. So the checker didn’t just confirm the proof. The process of getting it past the checker changed the author’s understanding of his own theorem.

The full formalization of the main theorem was finished on July 14, 2022, and announced on the Lean community blog the next day.⁶ That’s about a year and a half from challenge to completion, for one theorem, with a team of experts. Keep that number in mind for the costs section.

Polynomial Freiman-Ruzsa in three weeks

The Liquid Tensor Experiment showed that a proof assistant could handle cutting-edge math. The next project showed it could keep up with it.

In November 2023, Tim Gowers, Ben Green, Freddie Manners, and Terence Tao posted a paper proving Marton’s conjecture, also called the Polynomial Freiman-Ruzsa conjecture, a significant open problem in additive combinatorics.⁷ Within days, Tao launched a project to formalize it in Lean 4, organized with Yael Dillies and Bhavik Mehta. On November 18, less than a week in, he wrote that it was “proceeding quite well, with a significant fraction of the paper already either fully or partially formalized.”²

The project used a tool called Blueprint, which lets you write a human-readable outline of the proof where each lemma is a node in a dependency graph, linked to its Lean code. Nodes turn green as they’re formalized. This matters more than it sounds. It turns one huge proof into many small, independent tasks, so people who have never met can each take a node, and Tao noted in that same post that pull requests were already being approved from contributors who hadn’t met each other.² Lean checking each piece makes that kind of distributed work easier to coordinate, though people still review definitions and statements.

On December 5, Tao announced the formalization was complete. Lance Fortnow summarized it the next day on the Computational Complexity blog: “The process from paper to formalization took about three weeks.”⁸ Compare that to the year and a half for the Liquid Tensor Experiment. My guess is that part of the difference is that additive combinatorics needed less heavy machinery than Scholze’s work, and part is that Lean 4, Mathlib, and the community’s workflow had matured. Buzzard makes a similar point, that in some areas like combinatorics “modern breakthroughs can be formalised in real time.”⁹ Either way, a major new theorem was machine-checked before most people had finished reading the paper.

Fermat, and building the road before driving on it

If PFR shows what’s possible when the prerequisites already exist, Kevin Buzzard’s Fermat’s Last Theorem project shows what happens when they don’t.

Buzzard announced the project in April 2024 on the Lean community blog, and it’s funded by the UK’s Engineering and Physical Sciences Research Council under grant EP/Y022904/1.⁹¹⁰ He’s funded “for the first five years of the project,” and he’s careful about what those five years are for. The goal isn’t to formalize the entire proof from scratch. In his words, “my first goal is to reduce FLT to claims which were known to mathematicians by the end of the 1980s.”⁹ The route follows a modern version of the Wiles and Taylor-Wiles argument, not the original 1990s paper.¹¹

The most telling line in his announcement is about the library. He attends the London Number Theory Seminar regularly, and he wrote that “most weeks I note that Lean does not know enough modern mathematical definitions to even state the results announced in the seminar.”⁹ Not prove. State. Before you can check a proof about modular forms or Galois representations, someone has to define them in Lean, prove all the basic facts about them, and get it into Mathlib in a form other people can build on. A large part of the FLT project is that infrastructure work.

So FLT is a long bet. As of the date I’m writing this, the project is still in progress,¹⁰ and the honest summary is that a computer-checked proof of Fermat’s Last Theorem doesn’t exist yet. What exists is a growing pile of verified modern number theory that didn’t exist two years ago.

The Equational Theories Project

The fourth project is the one that I think says the most about where AI fits.

In September 2024, Tao proposed a “pilot project in universal algebra to explore new ways to collaborate and use machine assistance.”¹² The math is deliberately simple to state. A magma is a set with one binary operation and no other rules. An equational law is something like x * y = y * x. The question is: for every pair of simple laws, does the first one imply the second? Tao proposed looking at every law where the operation appears at most four times, and the enumeration came out to 4,694 laws.¹²

That’s 22,028,942 ordered pairs, each needing either a proof or a counterexample. No human team is going to review twenty-two million proofs by hand. That was the point. Tao pitched it as a test of whether Lean could let professionals, amateurs, and automated tools all contribute to one project, with the checker as the referee.¹²

It worked. The project’s paper reports that it hit its main goal on April 14, 2025, with every one of those implications settled and every proof or refutation formalized in Lean, from “a combination of human-generated and automated proofs.”¹ The paper has 34 authors. Many counterexamples came from brute-force search over small finite magmas, automated theorem provers handled a lot of the rest, and the stubborn cases took human cleverness.¹ And none of it required anyone to trust a contributor they’d never met, or to trust that a particular automated tool was bug-free. Lean checked the output, not the source.

The paper also says plainly why the older crowdsourcing model wouldn’t have worked: the Polymath projects “required human moderators to review and integrate the contributions of the participants, which clearly would not scale” to something this size.¹ I think that sentence describes the AI situation exactly, just with different contributors.

Plausible text versus checked text

Here’s the argument.

A language model is trained to produce text that looks like the text it was trained on. For most tasks that’s what you want, and for math it’s dangerous, because a wrong proof and a right proof can look almost identical. A missing case, a sign error, an “obviously” covering something false. These are the errors that read fluently.

There’s good evidence this is a real problem and not a hypothetical one. In March 2025, a group of researchers graded frontier models on the 2025 USA Math Olympiad, with human judges reading full proofs rather than just checking final answers. Their paper is called “Proof or Bluff?”, which is a fair summary of the finding: “only Gemini-2.5-Pro achieves a non-trivial score of 25%, while all other models achieve less than 5%.”¹³ The paper points out that the leading model had scored comparably to top human competitors on benchmarks that only check final numerical answers.¹³ When someone read the reasoning, most of it didn’t hold up.

Models have improved a lot since then. In July 2025, Google DeepMind reported that an advanced version of Gemini Deep Think scored 35 out of 42 at the International Mathematical Olympiad, gold-medal level, and that it “operated end-to-end in natural language.”¹⁴ That’s a genuinely impressive result. But look at how it was verified: IMO coordinators graded the proofs by hand, the same way they grade students.¹⁴ That works for six problems. It doesn’t work for six thousand, or for a research paper nobody has the time to read line by line.

Compare that with AlphaProof, which DeepMind announced a year earlier in July 2024. It worked in Lean. Together with AlphaGeometry 2, it solved four of the six 2024 IMO problems for a silver-medal score, though some problems took up to three days, far beyond the contest’s time limit.¹⁵ In raw performance it was the weaker result. In trustworthiness it was the stronger one, because its proofs were checked by a machine that cannot be talked into anything.

This is why I think proof-checking matters more than proof-finding. Proof-finding by AI is getting better fast, but its output is only as trustworthy as the human who reads it, and human reading doesn’t scale. A checker changes the economics. Invalid formal derivations get rejected automatically, reducing the manual checking needed during search, so you can let a model try a thousand times and only look at the one that passes. The model can be as unreliable as it likes in the search, as long as the final artifact is checked.

That’s also why the Equational Theories Project matters for this argument even though it isn’t really an AI project. It’s a demonstration that you can run a mathematical effort where the contributors are numerous and untrusted, and still trust the result. That’s exactly the setting AI puts us in.

I think this is the real difference between AI-for-math and AI-for-almost-everything-else. If a model writes a legal brief or a medical summary, there’s no kernel you can run it through. You’re back to a human reading carefully and hoping they caught everything. Code is the closest cousin, since tests and type checkers help, but tests check the cases someone thought of and a type checker checks shapes, not full correctness. A Lean proof of a correctly stated theorem is the rare case where “the machine accepted it” really does mean “it’s true,” modulo a small, heavily scrutinized kernel.

A model can produce a convincing answer to a different question from the one we asked. Formal checking gives us a useful way to catch that: a proof of a different statement will not pass against the intended statement. We still have to get that intended statement right first.

What it costs

None of this is free, and the people closest to formalization are the most honest about that.

Formalization is slow. The Liquid Tensor Experiment took about a year and a half for one theorem.⁴⁶ PFR took three weeks, but with a field whose prerequisites were mostly already in Mathlib and with Tao himself driving it.⁸ FLT is funded for five years just to get to a reduction to 1980s results.⁹

Formal proofs are long. There’s an old measure for this called the de Bruijn factor, named after N.G. de Bruijn, who described a roughly constant “loss factor” when translating ordinary math into his Automath system. Freek Wiedijk defines it as “the quotient of the size of a formalization of a mathematical text and the size of its informal original,” and for the examples he measured, it came out to about four.¹⁶ That historical ratio is useful context, not a reliable way to predict the size of a modern Lean project. Modern automation helps, but the overhead hasn’t gone away.

The library has gaps. Buzzard’s line about Lean not being able to even state seminar results is the sharpest version of this.⁹ Most of the cost of formalizing a new research result isn’t the proof itself. It’s building the definitions and basic theory the proof depends on. An AI that can write Lean proofs still needs the library to exist, and in a lot of modern math it doesn’t yet.

The checker only checks what you stated. This is the one I think gets glossed over most in AI discussions. The Equational Theories Project paper puts it directly: “The kernel checks proofs against a given specification,” and if the formal statement is flawed, “a correct and verified proof of this theorem would be mathematically meaningless.”¹ Lean guarantees the proof matches the statement. It can’t guarantee the statement matches what you meant.

This matters a lot for AI. If a model is allowed to write both the statement and the proof, it can quietly prove something easier than what you asked for, and Lean will happily accept it. For the 2024 IMO, DeepMind didn’t let AlphaProof do that: the blog post says “the problems were manually translated into formal mathematical language” before the system started.¹⁵ That’s the right call, and it shows where the human work moves. With a checker, you don’t need an expert to read the proof. You still need an expert to read the statement and the definitions behind it. That’s far less work (a theorem statement is usually a few lines, the proof can be thousands), but it isn’t zero, and anyone who says “verified by Lean” without saying who checked the statement is overselling.

There are smaller caveats too. Lean lets users add declarations without checking them, and the ETP paper notes that a verified proof is trusted “modulo the correctness of the kernel implementation.”¹ I mention them because the claim I’m making is strong, and strong claims should come with their footnotes.

Where I land

The possibility of getting a useful argument from a model is exciting. Being able to check that argument changes what we can do with it: we can take a surprising suggestion seriously without having to trust whoever produced it.

I wonder what mathematical collaboration could look like if more people could contribute ideas this way. There would still be work in stating the problem correctly, writing the proof, and understanding why it works. But a reliable way to check contributions could make it easier to explore ideas that would otherwise be too costly to review. I’d want the explanation to grow alongside the proof, so the result becomes something people can use.

Sources