Can Computers Be Mathematicians?
The Joy of Why
Steven Strogatz, Janna Levin and Quanta Magazine
4.9 • 577 Ratings
🗓️ 29 June 2022
⏱️ 33 minutes
🧾️ Download transcript
Summary
Artificial intelligence has bested humans at problem-solving tasks including games like chess and Go. Is mathematics research next? Steven Strogatz speaks with Kevin Buzzard, professor of pure mathematics at Imperial College London, to learn about the ongoing multidisciplinary effort to translate math into language that computers understand.
Transcript
Click on a timestamp to play from that location
| 0:00.0 | I'm Steve Strogatz, and this is the joy of why. |
| 0:07.7 | A podcast from Quantum Magazine that takes you into some of the biggest unanswered questions in science and math today. |
| 0:14.8 | In this episode, we're going to be talking about the future of computers in mathematics. |
| 0:19.6 | How much math can a computer do? |
| 0:22.2 | And could computers ever get really good at it, |
| 0:25.0 | maybe better than the best human mathematicians? |
| 0:28.1 | If that sounds far-fetched, well, just remember what happened in chess not so long ago. |
| 0:34.1 | You probably heard about an IBM computer called Deep Blue, which managed to beat the best human |
| 0:40.0 | chess player in the world, Gary Kasparov, back in 1997. Deep Blue, of course, being a computer, |
| 0:46.9 | was very fast. It could evaluate 200 million chess positions a second. And it based its |
| 0:53.7 | evaluations of those positions on a gigantic |
| 0:56.7 | library of chess knowledge that its programmers had built into it. Now, in a similar fashion, |
| 1:02.7 | a small but growing community of mathematicians has been busy writing code in a programming |
| 1:07.7 | language called Lean. They're building a library of math knowledge for |
| 1:12.5 | lean to reference to help human mathematicians check their proofs. Armed with the knowledge of |
| 1:17.7 | algebra, geometry, and logic, these programs, known as proof assistance. Do the busy work for people, |
| 1:26.2 | checking their work rigorously. |
| 1:28.1 | This frees up time and mental space for mathematicians to be more creative. |
| 1:33.0 | Recently, Lean helped one of the world's greatest mathematicians, Peter Schulze, |
| 1:38.0 | verify the accuracy of a complicated proof that he was working on. |
| 1:42.0 | There's a juicy story behind that, which we'll get to, but it was |
| 1:45.2 | kind of a big public relations win for this software. So the question is, what can computers do |
... |
Please login to see the full transcript.
Disclaimer: The podcast and artwork embedded on this page are from Steven Strogatz, Janna Levin and Quanta Magazine, and are the property of its owner and not affiliated with or endorsed by Tapesearch.
Generated transcripts are the property of Steven Strogatz, Janna Levin and Quanta Magazine and are distributed freely under the Fair Use doctrine. Transcripts generated by Tapesearch are not guaranteed to be accurate.
Copyright © Tapesearch 2026.