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

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: read.compose.llc
• The Kickstarter page for it: kickstarter.com/projects/ryanlpeterman/compose…

Podcast links:

• YouTube: youtu.be/KzdYKeAqWhY
• Apple: podcasts.apple.com/us/podcast/the-peterman-pod…
• Transcript: developing.dev/p/creator-of-lean-the-end-of-ha…

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 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: en.wikipedia.org/wiki/Leonardo_de_Moura
• Website: leodemoura.github.io
• GitHub: github.com/leodemoura
• LinkedIn: linkedin.com/in/leonardo-de-moura-26a27b5
• X/Twitter: x.com/Leonard41111588

Where to find Ryan:

• Newsletter: developing.dev
• X/Twitter: x.com/ryanlpeterman
• LinkedIn: linkedin.com/in/ryanlpeterman
• Threads: threads.com/@ryanlpeterman
• Instagram: instagram.com/ryanlpeterman
• TikTok: tiktok.com/@ryanlpeterman

Referenced in this episode:

• Lean 4: github.com/leanprover/lean4
• Mathlib: Lean Mathematical Library: github.com/leanprover-community/mathlib4
• Lean4Lean: github.com/digama0/lean4lean
• Liquid Tensor Experiment: xenaproject.wordpress.com/2020/12/05/liquid-te…
• Veil protocol verification language: veil.dev
• Z3 theorem prover: github.com/Z3Prover/z3
• seL4 formally verified microkernel: github.com/seL4/seL4