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: parallel.ai/mlst?utm_source=creator&utm_me… 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] Lean00:01:24]" rel="nofollow noopener ugc" target="_blank">lean-lang.org/[00:01:24] Mathlib00:12:09]" rel="nofollow noopener ugc" target="_blank">github.com/leanprover-community/mathlib4[00:12… nanoda_lib00:12:19]" rel="nofollow noopener ugc" target="_blank">github.com/ammkrn/nanoda_lib[00:12:19] CollatzLean00:13:06]" rel="nofollow noopener ugc" target="_blank">github.com/xrchz/CollatzLean/blob/a79357462a33… Lean issue 1457600:13:21]" rel="nofollow noopener ugc" target="_blank">github.com/leanprover/lean4/issues/14576[00:13… Lean pull request 1457700:13:45]" rel="nofollow noopener ugc" target="_blank">github.com/leanprover/lean4/pull/14577[00:13:45] nanoda_lib pull request 2200:15:33]" rel="nofollow noopener ugc" target="_blank">github.com/ammkrn/nanoda_lib/pull/22[00:15:33] Lean comparator00:18:02]" rel="nofollow noopener ugc" target="_blank">github.com/leanprover/comparator[00:18:02] Lean4Lean00:19:50]" rel="nofollow noopener ugc" target="_blank">github.com/digama0/lean4lean[00:19:50] ARC-AGI-300:21:59]" rel="nofollow noopener ugc" target="_blank">arcprize.org/arc-agi/3[00:21:59] lean-zip00:29:45]" rel="nofollow noopener ugc" target="_blank">github.com/kim-em/lean-zip[00:29:45] CompCert00:29:45]" rel="nofollow noopener ugc" target="_blank">compcert.org/[00:29:45] seL400:30:23]" rel="nofollow noopener ugc" target="_blank">sel4.org/[00:30:23] Z300:38:10]" rel="nofollow noopener ugc" target="_blank">github.com/Z3Prover/z3[00:38:10] Veil00:38:10]" rel="nofollow noopener ugc" target="_blank">github.com/verse-lab/veil[00:38:10] Velvet00:00:52]" rel="nofollow noopener ugc" target="_blank">github.com/verse-lab/velvetorganization:[00:00… Lean FRO00:42:39]" rel="nofollow noopener ugc" target="_blank">lean-lang.org/fro/[00:42:39] Mathlib Initiative00:05:11]" rel="nofollow noopener ugc" target="_blank">mathlib-initiative.org/about/person:[00:05:11] Ilya Sergey00:10:31]" rel="nofollow noopener ugc" target="_blank">ilyasergey.net/[00:10:31] Joachim Breitner00:32:58]" rel="nofollow noopener ugc" target="_blank">joachim-breitner.de/[00:32:58] Adam Chlipala00:38:42]" rel="nofollow noopener ugc" target="_blank">adam.chlipala.net/[00:38:42] Kevin Buzzard01:10:16]" rel="nofollow noopener ugc" target="_blank">ma.imperial.ac.uk/~buzzard/[01:10:16] Terence Tao00:08:19]" rel="nofollow noopener ugc" target="_blank">terrytao.wordpress.com/book:[00:08:19] The Proof in the Code00:10:05]" rel="nofollow noopener ugc" target="_blank">us.macmillan.com/books/9780374620059/theproofi… Brandolini's law00:45:33]" rel="nofollow noopener ugc" target="_blank">en.wikipedia.org/wiki/Brandolini%27s_law[00:45… A new result on unit distances01:01:08]" rel="nofollow noopener ugc" target="_blank">openai.com/index/model-disproves-discrete-geom… Fermat's Last Theorem formalisation00:34:36]" rel="nofollow noopener ugc" target="_blank">imperialcollegelondon.github.io/FLT/paper:[00:… The Lean 4 theorem prover and programming languagedoi.org/10.1007/978-3-030-79876-5_37---RESCRIP…