The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math (w/ Kevin Hartnett)
Published: June 24, 2026
Duration: 45:38
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 Significance
03:18 The Journey of Writing the Book
05:13 Human Element in Mathematical...