How do you teach mathematics to an artificial intelligence? AI has already bested humans at various problem-solving tasks, including games like chess and Go. But before any task can be tackled by a machine, it must be reinterpreted as directions in language that computers can understand. For the last few years, researchers and amateurs all over the world have worked together to translate the essential axioms of mathematics into a programming language called Lean. Armed with this knowledge, theorem-proving programs that understand Lean have begun helping some of the world’s greatest mathematicians verify their work. Steven Strogatz speaks with Kevin Buzzard, professor of pure mathematics at Imperial College London, about the effort to “teach” math to Lean — and how projects like this one could shape the future of math.
“The Joy of Why” is a podcast from Quanta Magazine, an editorially independent publication supported by the Simons Foundation. Funding decisions by the Simons Foundation have no influence on the selection of topics, guests, or other editorial decisions in this podcast or in Quanta Magazine. “The Joy of Why” is produced by Susan Valot and Polly Stryker. Our editors are John Rennie and Thomas Lin, with support by Matt Carlstrom, Annie Melchor and Leila Sloman. Our theme music was composed by Richie Johnson. Our logo is by Jackie King, and artwork for the episodes is by Michael Driver and Samuel Velasco. Our host is Steven Strogatz. If you have any questions or comments for us, please email us at quanta@simonsfoundation.org.