Lean creator Leo de Moura: AI now writes 50-million-line proofs, so verification is the bottleneck
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Ben Lorica talks with Leo de Moura, creator of Lean and a VP at AWS, about why machine-checked proofs matter once AI can generate code faster than anyone can review it. De Moura describes AI porting zlib to Lean, Anthropic's 13-million-line proof of Fermat's Last Theorem, and Claude Code finding real bugs in itself. The catch: someone still has to confirm the formal model faithfully matches the code.
Mathlib took 10 years, written by humans, to go from zero to 2.5 million lines. And now there are people writing proofs—that's AI writing the proofs—that are 50 million lines.
- chamomeal
What do people think of property based testing? I’ve set up a few property based tests and it feels almost like formal verification.
I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious setup, but LLMs solve that.
I haven’t seen much discussion around PBTs lately, but you get a ton of bang for your buck in the LLM age
- wbeckler
I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.
This is how formal methods can constrain AI for large systems.
We're doing this at the Open Markets Initiative, where we've generated millions of lines of Lean 4, TLA+, and Rocq that ensure that our open source electronic trading protocol code is accurate. We didn't expect it but the Lean prover did identify some incorrect steps.
- PandaRider
> ... But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.
Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)
- fspeech
Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean would ensure that the translation is correct.
- zujkas
Nobody verifies it because there isn't a ZFS axiom system for software development and you first need a spec to prove anything-
Then perhaps fix Lean's type system, which isn't really understood and has holes.
Can these AI-monied people shut up for a single hour?