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: Cold open: the green checkmark can lie Cathedral or bazaar: who controls Lean's core? Why Lean's core stays small and protected The Slack purge, Brandolini's law and the Lean FRO The Collatz exploit: two kernels, two bugs More kernels, reward hacking and safety by transparency Sponsor: Parallel Kim Morrison, Claude and the zlib proof Can we specify complex systems? Specs change: proofs are cheaper to redo with AI From Lean 1 to Lean 4 Dependent types in plain terms Lean 4's extensibility and Mathlib's growth Mathlib as infrastructure: Formal Frontiers Creativity, abstraction and nut-sniping Breadcrumbs, not learning: what AI agents lack Competence without comprehension, and verified guardrails Is the human still the author? AlphaProof, LLMs and why certificates still matter What's next for Lean, and its legacy How to start learning Lean---REFERENCES:tool:[] Leanhttps://lean-lang.org/[] Mathlibhttps://github.com/leanprover-community/mathlib4[] nanoda_libhttps://github.com/ammkrn/nanoda_lib[] CollatzLeanhttps://github.com/xrchz/CollatzLean/blob/a79357462a33d2a6babd4cf6c8d8bcd25425d653/README.md[] Lean issue 14576https://github.com/leanprover/lean4/issues/14576[] Lean pull request 14577https://github.com/leanprover/lean4/pull/14577[] nanoda_lib pull request 22https://github.com/ammkrn/nanoda_lib/pull/22[] Lean comparatorhttps://github.com/leanprover/comparator[] Lean4Leanhttps://github.com/digama0/lean4lean[] ARC-AGI-3https://arcprize.org/arc-agi/3[] lean-ziphttps://github.com/kim-em/lean-zip[] CompCerthttps://compcert.org/[] seL4https://www.sel4.org/[] Z3https://github.com/Z3Prover/z3[] Veilhttps://github.com/verse-lab/veil[] Velvethttps://github.com/verse-lab/velvetorganization:[] Lean FROhttps://lean-lang.org/fro/[] Mathlib Initiativehttps://mathlib-initiative.org/about/person:[] Ilya Sergeyhttps://ilyasergey.net/[] Joachim Breitnerhttps://www.joachim-breitner.de/[] Adam Chlipalahttps://adam.chlipala.net/[] Kevin Buzzardhttps://www.ma.imperial.ac.uk/~buzzard/[] Terence Taohttps://terrytao.wordpress.com/book:[] The Proof in the Codehttps://us.macmillan.com/books/9780374620059/theproofinthecode/other:[] Brandolini's lawhttps://en.wikipedia.org/wiki/Brandolini%27s_law[] A new result on unit distanceshttps://openai.com/index/model-disproves-discrete-geometry-conjecture/[] Fermat's Last Theorem formalisationhttps://imperialcollegelondon.github.io/FLT/paper:[] 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
