About this episode
Kevin Buzzard discusses the potential of computers and AI in proving theorems and their implications for mathematics.
Kevin Buzzard: Will Computers prove theorems? Will computers one day replace human mathematicians? Is this just around the corner, or decades away? Can neural networks spot patterns which humans have missed? Currently language models are great for brainstorming big ideas but are very poor when it comes to details. Can integrating a language model with a theorem prover like Lean solve these problems? Is the modern mathematical literature riddled with errors, and is it feasible to hope that a machine might find and even fix them? Is it possible to teach a computer the proof of Fermat's Last Theorem? And what do mathematicians make of all this? I'll talk about how modern developments in AI and theorem provers are beginning to affect mathematics.
People in this episode
Guest: Kevin Buzzard
Topics covered
- computers
- theorems
- mathematics
- AI
- neural networks
- theorem provers
Keywords
- computers
- theorems
- AI
- neural networks
- mathematics
- Fermat's Last Theorem
- theorem provers
Mentioned in this episode
Organizations: Lean
Books & works: Fermat's Last Theorem
More episodes of Strachey Lectures
- Hardening Digital Infrastructure: Two Examples · May 27, 2026 · 1h 2m
- An AI stack: from scaling AI workloads to evaluating LLMs · February 26, 2026 · 56 min
- Advances in Garbled Circuits · October 27, 2025 · 48 min
- Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI · May 15, 2025 · 47 min
- Privacy, Verification, Robustness: A Cryptographer's perspective on ML · March 11, 2025 · 1h 4m
- From probabilistic bisimulation to representation learning via metrics · December 2, 2024 · 55 min
Explore listener stats, chart rankings, contacts and more on the Strachey Lectures podcast page.