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. --- --- 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