The 'Truth Machine' That Is Changing Math
6/16/202634 min
The groundbreaking proof assistant Lean acts as a sort of automatic quality control. It’s gaining ground in the math world — in part because it can interact with AI to open new avenues of inquiry. But there are concerns, too. On this episode of The Quanta Podcast, host Samir Patel speaks with author Kevin Harnett about his new book, the first release from Quanta Books, “The Proof in the Code.” It was featured in a recent excerpt for Quanta Magazine.
Each week on The Quanta Podcast, Quanta Magazine editor in chief Samir Patel speaks with the people behind the award-winning publication to navigate through some of the most important and mind-expanding questions in science and math.
Clips
Transcript preview
First 90 secondsSpeaker 10:01
What if your discovery of a natural gene editing mechanism launched a revolution?
Samir Patel· Host0:06
What if your abstract math proofs had unexpected connections to the real world?
Speaker 10:11
What if your Nobel Prize-winning work on the expanding universe was just the beginning of the story?
Samir Patel· Host0:17
And what if you joined us, Steve Strogatz- And Janna Levin ... to learn about all of this and much more on one podcast?
Speaker 10:24
Listen to season five of Quanta Magazine's- The Joy of Why. New episodes drop every other Thursday starting June 11th.
Samir Patel· Host0:33
[instrumental music plays] We at Quanta are always thinking about math, but this year in particular, we've been really focused on it. Honestly, there's just a lot going on. This summer we'll see the International Congress of Mathematicians and the awarding of the Fields Medals, which happens only every four years, same as the World Cup. In fact, it's happening the week after the World Cup final. We ran a special series on the foundations of math and have been regularly covering how AI is changing the field. And also Quanta Books, in partnership with Farrar, Straus and Giroux, has just released its debut book, and it's about math too, specifically the proof assistant called Lean. [drum music plays] Welcome to the Quanta Podcast, where we explore the frontiers of fundamental science and math. I'm Samir Patel,