Creator of Lean: Handwritten Math Will Change Dramatically
This title could be clearer and more informative.Try out Clickbait Shieldfor free (5 uses left this month).
Leonardo de Moura, creator of the Lean proof assistant, discusses how Lean works as both a programming language and formal verification tool. He explains how AI is dramatically lowering the cost of writing and maintaining formal proofs — a task that previously required 10x the effort of writing the code itself. Key examples include a colleague formalizing and verifying the zlib compression library in one week using AI, and a 1-million-line formal proof of the unit distance conjecture completed in roughly two weeks. De Moura also covers how Lean differs from the Z3 SMT solver he built at Microsoft Research, how AlphaProof and other AI systems use Lean as a game-like environment for reinforcement learning, and why he believes handwritten math will change dramatically but not disappear entirely as AI-human hybrid workflows become the norm.
Questions this post answers
How does AlphaProof use Lean to solve IMO problems?
AlphaProof treats Lean proof construction as a single-player game. Each IMO problem is first translated into a Lean theorem statement using mathlib. The AI then applies tactic steps — rewriting rules, simplifications — and observes the changing proof state (the Infoview) as feedback. Reinforcement learning trains the model to reach 'no goals left', meaning the proof is complete and machine-verified. DeepMind achieved a silver medal at IMO 2024 this way. Teams working on AI math reasoning track Lean ecosystem developments on daily.dev.
What is the difference between Lean and Z3 as theorem provers?
Lean is an interactive proof assistant where users (or AI) guide proofs step by step using a tactic language, giving full control over the proof structure. Z3 is a fully automatic SMT solver — you submit constraints and it either finds a counterexample or declares unsatisfiability with no user guidance. Z3 excels at bug-finding but struggles to prove absence of bugs; Lean was created specifically to fill that gap. Developers choosing between formal verification tools find comparative discussions like this on daily.dev.
How long did it take to formally verify the zlib compression library in Lean using AI?
A researcher named Kim Morrison translated the C zlib library into Lean, ensured it passed zlib's test suites, and proved the core round-trip property — that compressing then decompressing data returns the original — in approximately one week using AI assistance. After verification, further optimization was constrained to preserve all proved properties, preventing regressions. Engineers exploring AI-assisted formal verification for production codebases follow this space on daily.dev.