What Does the Fourth Dimension Actually Look Like?
Oct 1, 2026
The Joy of Why
Can Computers Be Mathematicians?
Mathematics and Computer Science podcast with Kevin Buzzard
The Joy of Why, Hosted by Steven Strogatz
Wednesday 33 min
About
Kevin Buzzard of Imperial College London joins Steven Strogatz to discuss Lean, formal proof assistants and the effort to encode mathematical knowledge in a computer-readable library. They explore how computers verify difficult arguments, the distinction between Lean and its mathematical library, the formalization of work by Peter Scholze and Dustin Clausen, and the prospects and limits of computers creating new mathematics.
Topics
Related episodes
- Live from ICM 2026: What Is Math For in the Age of AI?Sep 3, 2026 · 53 min
- How Do Mathematicians Know Their Proofs Are Correct?Jul 13, 2022 · 28 min
- What Makes for ‘Good’ Mathematics?Feb 1, 2024 · 36 min
- Lab Notes: The AI maths warsSep 15, 2026 · 13 min
- Is There Math Beyond the Equal Sign?Mar 22, 2023 · 50 min
More from The Joy of Why
All episodesWhere Does the Quantum World End and Ours Begin?
Sep 17, 2026The Joy of WhyHow Does Touch Lead To Pain Or Pleasure?
Aug 6, 2026The Joy of WhyHow Fast Is the Universe Really Expanding?
Jul 23, 2026The Joy of Why