Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura
Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura  
Podcast: The Peterman Pod
Published On: Mon Aug 10 2026
Description: 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.• My ergonomic keyboard project I mentioned, you can follow along here: https://read.compose.llc/• The Kickstarter page for it: https://www.kickstarter.com/projects/ryanlpeterman/compose-simple-ergonomics-beautifully-donePodcast links:• YouTube: https://youtu.be/KzdYKeAqWhY• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835• Transcript: https://www.developing.dev/p/creator-of-lean-the-end-of-handwrittenThank you to this episode's sponsor for supporting my work:• 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/Timestamps:(00:00) Intro(00:28) How formal verification works(05:21) A new way of writing software(13:15) Proof assistants vs programming languages(21:06) How Lean has assisted in mathematical breakthroughs(32:03) When is it worth formalizing software(33:29) How Lean will impact handwritten math(38:55) The Z3 theorem prover project he started(45:44) The most technically challenging work of his career(51:10) Lean vs its competitors(01:00:37) The future of Lean(01:04:10) Technical book recommendations(01:06:15) Advice for his younger self(01:07:10) OutroWhere to find Leonardo:• Wikipedia: https://en.wikipedia.org/wiki/Leonardo_de_Moura• Website: https://leodemoura.github.io/• GitHub: https://github.com/leodemoura• LinkedIn: https://www.linkedin.com/in/leonardo-de-moura-26a27b5/• X/Twitter: https://x.com/Leonard41111588Where to find Ryan:• Newsletter: https://www.developing.dev/• X/Twitter: https://x.com/ryanlpeterman• LinkedIn: https://www.linkedin.com/in/ryanlpeterman/• Threads: https://www.threads.com/@ryanlpeterman• Instagram: https://www.instagram.com/ryanlpeterman• TikTok: https://www.tiktok.com/@ryanlpetermanReferenced in this episode:• Lean 4: https://github.com/leanprover/lean4• Mathlib: Lean Mathematical Library: https://github.com/leanprover-community/mathlib4• Lean4Lean: https://github.com/digama0/lean4lean• Liquid Tensor Experiment: https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/• Veil protocol verification language: https://veil.dev/• Z3 theorem prover: https://github.com/Z3Prover/z3• seL4 formally verified microkernel: https://github.com/seL4/seL4