Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura
Notes de l’épisode
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-done
Podcast 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-handwritten
Thank 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) Outro
Where 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/Leonard41111588
Where 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/@ryanlpeterman
Referenced 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