Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura
About this episode
Ryan Peterman interviews Leonardo de Moura about Lean and its impact on software and mathematics.
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…
Sponsors
WorkOS
More episodes of The Peterman Pod
- How Anthropic Builds And How Engineering Will Change Soon | Thariq Shihipar
- Creator of Scala: Comparing Languages And How AI Will Impact Them | Martin Odersky
- Sergey Levine: Current State of Humanoid Robotics, China & Future Predictions
- Creator of TypeScript: 10x Faster Typescript, Why AI Won't Replace SWEs | Anders Hejlsberg
- Creator of Lua: Scripting, Programming Languages, Predictions | Roberto Ierusalimschy
- Turing Award Winner: Early AI, LLM Predictions, Causality | Judea Pearl
Explore listener stats, chart rankings, contacts and more on the The Peterman Pod podcast page.