The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math (w/ Kevin Hartnett)

In this episode, Autumn and Noah talk with Kevin Hartnett about why mathematicians are willing to spend years reducing an idea to a level of detail a machine can check, whether formal verification can catch an AI that's technically correct but fundamentally misaligned, the cold-start problem that kept earlier theorem-provers niche, and what it means for the future of mathematical trust once AI can generate proofs faster than any human community can read them.Timeline:00:00 Introduction to Lean and Its Significance03:18 The Journey of Writing the Book05:13 Human Element in Mathematical Formalization06:57 Understanding Formal Proofs in Mathematics11:21 The Origins of Lean and Its Purpose13:03 Misalignment in Software Specifications14:39 Building Mathematical Libraries in Lean17:23 Ensuring Accuracy in Mathematical Foundations22:00 Overcoming the Cold Start Problem in Lean Adoption24:36 The Future of Mathematical Proofs30:26 AI's Role in Mathematics38:29 Expanding Beyond Mathematics41:40 The Long-Term Impact of LeanThe Proof in the Code is out now from Quanta Books. (https://amzn.to/3SuNlJm)Follow Kevin Hartnett onX (https://x.com/KSHartnett) Bluesky (https://bsky.app/profile/kevinhartnett.bsky.social)Follow Breaking Math onSubstack (https://breakingmath.substack.com/)X (https://x.com/breakingmathpod)Instagram (https://www.instagram.com/breakingmathmedia/)Bluesky (https://bsky.app/profile/breakingmath.bsky.social)Website (https://www.breakingmath.io/)YouTube (https://www.youtube.com/@BreakingMathPod)Follow Noah onInstagram (https://www.instagram.com/profnoahgian/)X (https://x.com/ProfNoahGian)Bluesky (https://bsky.app/profile/profnoahgian.bsky.social)Follow Autumn onX (https://x.com/1autumn_leaf)Bluesky (https://bsky.app/profile/1autumnleaf.bsky.social)Instagram (https://www.instagram.com/1autumnleaf/)Substack (https://substack.com/@1autumnleaf)email: breakingmathpodcast@gmail.com