Using math to prove the correctness of computer programs, called formal methods, is perhaps the complete opposite of my usual interest in human–computer interaction. But they have fascinated me since my college years at Caltech, when I learned about them in my sophomore computer science class (a very unusual topic to cover at such an early stage). However, back then, you essentially had to prove the correctness of a program by hand, which was slow, tedious, and not practical. We played around with an early theorem prover, but it was clearly experimental.
So my interest was piqued when, thanks to an excerpt in Quanta Magazine, I learned about the book The Proof in the Code by Kevin Harnett, about the development of Lean, an interactive theorem prover that was originally targeted at proving the correctness of computer programs but has become the leading platform for formalizing mathematics. (OpenAI used Lean to verify its groundbreaking, and controversial, math proofs.) I’ve enjoyed the book so far, as it goes into the human stories behind Lean’s history.
But I wanted to learn more, so I’ve queued up a bunch of podcast episodes, mostly about Lean, but a few about other systems like TLA+ and formal methods in general. It’s almost 16 hours in total, and I’ve just started! In case you’re interested, here they are:
- Type Theory Forall
- Episode 26: Mechanizing Modern Mathematics — Kevin Buzzard (2023-01-16)
- Episode 33: Z3 and Lean, the Spiritual Journey — Leo de Moura (2023-09-09)
- Episode 38: Haskell, Lean, idris, and the Art of Writing — David Christiansen (2024-05-16)
- Episode 44: Theorem Prover Foundations, Lean4Lean, Metamath — Mario Carneiro (2024-11-06)
- Episode 64: TLA+, Quint, and Formal Verification in the Age of AI — Gabriela Moreira (2026-10-19)
- The Haskell Interlude
- Episode 55: Sebastian Ullrich (2024-08-16)
- Augmented Mind Podcast
- Episode 5: It’s Our Mathematics: AI, Verification, and the Future of Math — Jeremy Avigad (2026-06-09)
- Breaking Math