Who Checks a Proof No Human Can Read? — 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.---TIMESTAMPS:00:00:00 Cold open: the green checkmark can lie00:00:59 Cathedral or bazaar: who controls Lean's core?00:04:55 Why Lean's core stays small and protected00:08:07 The Slack purge, Brandolini's law and the Lean FRO00:11:12 The Collatz exploit: two kernels, two bugs00:16:44 More kernels, reward hacking and safety by transparency00:21:04 Sponsor: Parallel00:21:59 Kim Morrison, Claude and the zlib proof00:25:25 Can we specify complex systems?00:28:04 Specs change: proofs are cheaper to redo with AI00:31:27 From Lean 1 to Lean 400:34:57 Dependent types in plain terms00:37:25 Lean 4's extensibility and Mathlib's growth00:41:44 Mathlib as infrastructure: Formal Frontiers00:44:15 Creativity, abstraction and nut-sniping00:48:46 Breadcrumbs, not learning: what AI agents lack00:53:03 Competence without comprehension, and verified guardrails00:56:21 Is the human still the author?01:01:44 AlphaProof, LLMs and why certificates still matter01:06:38 What's next for Lean, and its legacy01:11:42 How to start learning Lean---REFERENCES:tool:[00:00:48] Leanhttps://lean-lang.org/[00:01:24] Mathlibhttps://github.com/leanprover-community/mathlib4[00:12:09] nanoda_libhttps://github.com/ammkrn/nanoda_lib[00:12:19] CollatzLeanhttps://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/README.md[00:13:06] Lean issue 14576https://github.com/leanprover/lean4/issues/14576[00:13:21] Lean pull request 14577https://github.com/leanprover/lean4/pull/14577[00:13:45] nanoda_lib pull request 22https://github.com/ammkrn/nanoda_lib/pull/22[00:15:33] Lean comparatorhttps://github.com/leanprover/comparator[00:18:02] Lean4Leanhttps://github.com/digama0/lean4lean[00:19:50] ARC-AGI-3https://arcprize.org/arc-agi/3[00:21:59] lean-ziphttps://github.com/kim-em/lean-zip[00:29:45] CompCerthttps://compcert.org/[00:29:45] seL4https://www.sel4.org/[00:30:23] Z3https://github.com/Z3Prover/z3[00:38:10] Veilhttps://github.com/verse-lab/veil[00:38:10] Velvethttps://github.com/verse-lab/velvetorganization:[00:00:52] Lean FROhttps://lean-lang.org/fro/[00:42:39] Mathlib Initiativehttps://mathlib-initiative.org/about/person:[00:05:11] Ilya Sergeyhttps://ilyasergey.net/[00:10:31] Joachim Breitnerhttps://www.joachim-breitner.de/[00:32:58] Adam Chlipalahttps://adam.chlipala.net/[00:38:42] Kevin Buzzardhttps://www.ma.imperial.ac.uk/~buzzard/[01:10:16] Terence Taohttps://terrytao.wordpress.com/book:[00:08:19] The Proof in the Codehttps://us.macmillan.com/books/9780374620059/theproofinthecode/other:[00:10:05] Brandolini's lawhttps://en.wikipedia.org/wiki/Brandolini%27s_law[00:45:33] A new result on unit distanceshttps://openai.com/index/model-disproves-discrete-geometry-conjecture/[01:01:08] Fermat's Last Theorem formalisationhttps://imperialcollegelondon.github.io/FLT/paper:[00:34:36] The Lean 4 theorem prover and programming languagehttps://doi.org/10.1007/978-3-030-79876-5_37---RESCRIPT:https://app.rescript.info/share/7d3d4a0059443236a01f6c9acbf4db58https://app.rescript.info/api/public/sessions/b007264c0ce89047/pdf