When the Referee of Mathematics Is Wrong — Leo de Moura
Leonardo de Moura created Lean and co-created Z3. --- This episode is sponsored by Parallel. Parallel, where agents find answers: web search, extraction and deep research APIs built for AI agents. Start free with the Parallel MCP server and $5 of credits every month: https://parallel.ai/mlst?utm_source=creator&utm_medium=podcast&utm_content=MLST --- Tim Scarfe talks with Leo about how Lean escaped its original audience, why dependent types and Mathlib made it useful to working mathematicians, and what happens when formal verification leaves the lab. De Moura explains the small trusted kernel and independent checkers, and gives his account of the recent Collatz incident, in which a purported proof was accepted by both Lean's official kernel and Nanoda, apparently by exploiting a different bug in each. The conversation then turns to AI-produced proofs and software. Claude agents rebuild zlib in Lean and the result is verified, yet the example exposes the loophole at the centre of the show: a proof only certifies the specification humans chose to write. De Moura describes proof search as a game, separates formal competence from mathematical understanding, and asks what authorship means when models can generate proofs at scale. The closing argument puts human responsibility upstream: choosing definitions, judging abstractions, curating Mathlib, inspecting certificates, and deciding which problems deserve effort. He also reflects on Lean's future beyond its founder and gives a practical starting point for new users. --- TIMESTAMPS: 00:00:00 Cold open: the green checkmark can lie 00:00:59 Cathedral or bazaar: who controls Lean's core? 00:04:55 Why Lean's core stays small and protected 00:08:07 The Slack purge, Brandolini's law and the Lean FRO 00:11:12 The Collatz exploit: two kernels, two bugs 00:16:44 More kernels, reward hacking and safety by transparency 00:21:04 Sponsor: Parallel 00:21:59 Kim Morrison, Claude and the zlib proof 00:25:25 Can we specify complex systems? 00:28:04 Specs change: proofs are cheaper to redo with AI 00:31:27 From Lean 1 to Lean 4 00:34:57 Dependent types in plain terms 00:37:25 Lean 4's extensibility and Mathlib's growth 00:41:44 Mathlib as infrastructure: Formal Frontiers 00:44:15 Creativity, abstraction and nut-sniping 00:48:46 Breadcrumbs, not learning: what AI agents lack 00:53:03 Competence without comprehension, and verified guardrails 00:56:21 Is the human still the author? 01:01:44 AlphaProof, LLMs and why certificates still matter 01:06:38 What's next for Lean, and its legacy 01:11:42 How to start learning Lean --- REFERENCES: tool: [00:00:48] Lean https://lean-lang.org/ [00:01:24] Mathlib https://github.com/leanprover-community/mathlib4 [00:12:09] nanoda_lib https://github.com/ammkrn/nanoda_lib [00:12:19] CollatzLean https://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/README.md [00:13:06] Lean issue 14576 https://github.com/leanprover/lean4/issues/14576 [00:13:21] Lean pull request 14577 https://github.com/leanprover/lean4/pull/14577 [00:13:45] nanoda_lib pull request 22 https://github.com/ammkrn/nanoda_lib/pull/22 [00:15:33] Lean comparator https://github.com/leanprover/comparator [00:18:02] Lean4Lean https://github.com/digama0/lean4lean [00:19:50] ARC-AGI-3 https://arcprize.org/arc-agi/3 [00:21:59] lean-zip https://github.com/kim-em/lean-zip [00:29:45] CompCert https://compcert.org/ [00:29:45] seL4 https://www.sel4.org/ [00:30:23] Z3 https://github.com/Z3Prover/z3 [00:38:10] Veil https://github.com/verse-lab/veil [00:38:10] Velvet https://github.com/verse-lab/velvet organization: [00:00:52] Lean FRO https://lean-lang.org/fro/ [00:42:39] Mathlib Initiative https://mathlib-initiative.org/about/ [01:11:42] Computerphile https://www.youtube.com/@Computerphile person: [00:05:11] Ilya Sergey https://ilyasergey.net/ [00:10:31] Joachim Breitner https://www.joachim-breitner.de/ [00:32:58] Adam Chlipala https://adam.chlipala.net/ [00:38:42] Kevin Buzzard https://www.ma.imperial.ac.uk/~buzzard/ [01:10:16] Terence Tao https://terrytao.wordpress.com/ book: [00:08:19] The Proof in the Code https://us.macmillan.com/books/9780374620059/theproofinthecode/ other: [00:10:05] Brandolini's law https://en.wikipedia.org/wiki/Brandolini%27s_law [00:45:33] A new result on unit distances https://openai.com/index/model-disproves-discrete-geometry-conjecture/ [01:01:08] Fermat's Last Theorem formalisation https://imperialcollegelondon.github.io/FLT/ paper: [00:34:36] The Lean 4 theorem prover and programming language https://doi.org/10.1007/978-3-030-79876-5_37 [01:02:06] AlphaProof https://doi.org/10.1038/s41586-025-09833-y [01:04:24] AlphaZero https://arxiv.org/abs/1712.01815 --- RESCRIPT: https://app.rescript.info/share/7d3d4a0059443236a01f6c9acbf4db58 https://app.rescript.info/api/public/sessions/b007264c0ce89047/pdf
