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 [https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/]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.