Robert George closed Part 2 with the paper that, in a sense, underwrites the others. Lean for Science argues that machine-checked formal proofs — long a niche of pure mathematics — are about to reshape three fields at once: mathematics, AI, and scientific computing. After a paper on self-play for theorem proving, this is the natural sequel: it explains why theorem proving is such fertile ground for AI in the first place.
A formal proof is one a computer can check line by line. If it passes the checker, it is correct — full stop. No referee, no "left as an exercise," no subtle gap discovered three years later. That single property is what makes formal proofs so powerful, and so useful to AI.
What Lean is
Lean is both a programming language and an interactive theorem prover, created by Leonardo de Moura. Thanks to dependent types, it can express mathematical statements as types: a proof of a theorem P is literally a value of type P. A small trusted proof checker then verifies that value. You can write ordinary programs in Lean, but you can also write theorems and proofs that the machine confirms with the same rigor it confirms a type.
The thing that makes Lean practical rather than academic is Mathlib — an enormous, community-built library of formalized mathematics, from basic algebra to deep modern results. Mathlib is to formal math what a standard library is to programming: the shared, verified foundation you build on instead of re-deriving the world from axioms every time.
Changing mathematics
Formalization is moving from a curiosity to a working method. Why mathematicians increasingly care:
- Certainty — a formalized proof has no gaps. Several famous results have been formalized after the fact precisely because the informal proofs were too long or intricate for any human to fully vet.
- Collaboration at scale — because the checker guarantees correctness, large groups can contribute pieces of a proof without a central genius verifying everyone's work by hand. Correctness composes.
- Search and reuse — a machine-readable library of theorems can be searched, mined, and recombined. AI tools are starting to help mathematicians find the right existing lemma, not just check new ones.
Changing AI — the key idea
This is the part that connects to everything else in the batch. AI reasoning has a trust problem: a model can produce a fluent, confident argument that is wrong, and checking it requires an expert. Formal proof removes the expert from the loop. If a model emits a proof and Lean accepts it, the proof is correct — the checker is an incorruptible ground-truth reward signal.
You cannot hallucinate a formal proof past the checker. That makes theorem proving the rare domain where an AI's output can be automatically, perfectly verified — which is exactly what reinforcement learning and self-play need to scale safely.
This is why formal theorem proving is such a magnet for AI research, and why the previous paper's self-play setup fits it so naturally: the Solver's success is judged by the checker, not by a fallible reward model that can be gamed. Generated proofs that pass are trustworthy training signal; those that fail are unambiguous negatives. It's the cleanest reward in machine learning, and it's driving systems that prove olympiad-level mathematics.
| Field | What formal proof changes | The mechanism |
|---|---|---|
| Mathematics | certainty, scale collaboration, searchable knowledge | Mathlib + the proof checker |
| AI | an incorruptible reward for reasoning; no hallucinated proof passes | checker as ground truth for RL / self-play |
| Scientific computing | bug-free code, proven to meet its specification | proofs attached to executable functions |
Changing scientific computing
The third leg is the least famous and maybe the most consequential. Scientific results increasingly rest on code — simulations, numerical solvers, data pipelines — and that code has bugs, some of which have quietly invalidated published findings. Because Lean is also a programming language, you can write a function and a machine-checked proof that it meets its specification: that the solver converges, that the numerical method respects its error bound, that the implementation matches the math.
Verified computation means correctness by proof rather than by testing. Tests sample inputs and hope; a proof covers all of them. For high-stakes scientific and engineering software — the kind where a bug is a retracted paper or a failed mission — that's a categorical upgrade. The Lean for Science initiative is the push to carry these methods out of pure math and into physics, chemistry, and computational science generally.
Why this was the closer
Because it ties the batch together. A world model of biology (paper 1) and a streaming voice agent (paper 3) are about capability; self-play (paper 2) is about how models improve. Lean for Science is about trust — the substrate that lets capability and self-improvement be verified rather than hoped for. As AI generates more of our mathematics, code, and scientific claims, the ability to machine-check what it produces stops being a luxury and becomes the foundation.
- For AI builders: formal verification is the cleanest reward signal you can give a reasoning model — wherever you can formalize the target, you can train against truth.
- For scientific software: proofs beat tests for the claims that matter most; Lean lets the proof live next to the code.
- For mathematics: formalization is becoming collaborative infrastructure, not a fringe hobby — and AI is now part of the workflow.
The honest caveats
Formalization is still expensive — turning an informal proof or a piece of scientific code into Lean can take far longer than writing it informally, and the skill is rare. Mathlib is huge but far from covering all of mathematics. And a proof only guarantees what its specification says: get the spec wrong and you've rigorously proven the wrong thing. The promise is real, but the bottleneck — the human cost of formalizing — is exactly where AI assistance is now being aimed.
The AlphaProof connection
This isn't theoretical. DeepMind's AlphaProof reached silver-medal performance at the International Mathematical Olympiad by generating candidate proofs in Lean and using the checker to filter and learn from them — exactly the loop described above. The checker turns mathematics into a domain where a model can practice billions of times against perfect feedback, the way game-playing agents practiced against the rules of Go. Self-Guided Self-Play (the previous paper) is a refinement of how to generate the practice problems for that loop. Read together, the two papers describe a full pipeline: a clean verifier (Lean) plus a non-degenerate curriculum (SGS) equals a reasoning model that improves against truth.
The broader bet is that any reasoning we can formalize, we can train against without a human in the loop — and formalization is the bottleneck AI is now being turned on to dissolve. It's a virtuous circle: AI helps formalize more mathematics; more formalized mathematics gives AI more verifiable ground to train on.
Where this is heading
The trajectory the talk sketches: formalization spreading from pure math into the sciences, AI assistants making the expensive act of formalizing cheaper, and verified components becoming standard in the software that underpins research and high-stakes engineering. The endgame isn't "computers do math instead of humans." It's a world where claims — mathematical, computational, eventually scientific — ship with a machine-checkable certificate, and where AI systems are trusted not because they sound right but because their output passed a checker. In an era of fluent, confident, occasionally-wrong models, that's the most valuable property there is.
The takeaway
A formal proof is correctness a machine can confirm, and that single property ripples outward: rigor and scale for mathematics, an incorruptible reward signal for AI reasoning, and bug-free guarantees for scientific computing. As models write more of our proofs, code, and claims, the checker becomes the thing we trust instead of the author. That's the quiet, foundational shift Lean for Science is betting on — and a fitting close to Part 2.