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: 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