Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura

<p>Leonardo de Moura is the creator of Lean and the Z3 theorem prover. I talked with him about how Lean works and why LLMs plus Lean will fundamentally change how we write software and do math.</p><p><br></p><p>• My ergonomic keyboard project I mentioned, you can follow along here: https://read.compose.llc/</p><p>• The Kickstarter page for it: https://www.kickstarter.com/projects/ryanlpeterman/compose-simple-ergonomics-beautifully-done</p><p><br></p><p>Podcast links:</p><p><br></p><p>• YouTube: https://youtu.be/KzdYKeAqWhY</p><p>• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835</p><p>• Transcript: https://www.developing.dev/p/creator-of-lean-the-end-of-handwritten</p><p><br></p><p>Thank you to this episode&#39;s sponsor for supporting my work:</p><p><br></p><p>• WorkOS: makes your app Enterprise Ready with easy to use APIs to add SSO, SCIM, RBAC, and more in just a few lines of code, check them out at https://workos.com/</p><p><br></p><p>Timestamps:</p><p><br></p><p>(00:00) Intro</p><p>(00:28) How formal verification works</p><p>(05:21) A new way of writing software</p><p>(13:15) Proof assistants vs programming languages</p><p>(21:06) How Lean has assisted in mathematical breakthroughs</p><p>(32:03) When is it worth formalizing software</p><p>(33:29) How Lean will impact handwritten math</p><p>(38:55) The Z3 theorem prover project he started</p><p>(45:44) The most technically challenging work of his career</p><p>(51:10) Lean vs its competitors</p><p>(01:00:37) The future of Lean</p><p>(01:04:10) Technical book recommendations</p><p>(01:06:15) Advice for his younger self</p><p>(01:07:10) Outro</p><p><br></p><p>Where to find Leonardo:</p><p><br></p><p>• Wikipedia: https://en.wikipedia.org/wiki/Leonardo_de_Moura</p><p>• Website: https://leodemoura.github.io/</p><p>• GitHub: https://github.com/leodemoura</p><p>• LinkedIn: https://www.linkedin.com/in/leonardo-de-moura-26a27b5/</p><p>• X/Twitter: https://x.com/Leonard41111588</p><p><br></p><p>Where to find Ryan:</p><p><br></p><p>• Newsletter: https://www.developing.dev/</p><p>• X/Twitter: https://x.com/ryanlpeterman</p><p>• LinkedIn: https://www.linkedin.com/in/ryanlpeterman/</p><p>• Threads: https://www.threads.com/@ryanlpeterman</p><p>• Instagram: https://www.instagram.com/ryanlpeterman</p><p>• TikTok: https://www.tiktok.com/@ryanlpeterman</p><p><br></p><p>Referenced in this episode:</p><p><br></p><p>• Lean 4: https://github.com/leanprover/lean4</p><p>• Mathlib: Lean Mathematical Library: https://github.com/leanprover-community/mathlib4</p><p>• Lean4Lean: https://github.com/digama0/lean4lean</p><p>• Liquid Tensor Experiment: https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/</p><p>• Veil protocol verification language: https://veil.dev/</p><p>• Z3 theorem prover: https://github.com/Z3Prover/z3</p><p>• seL4 formally verified microkernel: https://github.com/seL4/seL4</p>