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 Significance

03:18 The Journey of Writing the Book

05:13 Human Element in Mathematical Formalization

06:57 Understanding Formal Proofs in Mathematics

11:21 The Origins of Lean and Its Purpose

13:03 Misalignment in Software Specifications

14:39 Building Mathematical Libraries in Lean

17:23 Ensuring Accuracy in Mathematical Foundations

22:00 Overcoming the Cold Start Problem in Lean Adoption

24:36 The Future of Mathematical Proofs

30:26 AI's Role in Mathematics

38:29 Expanding Beyond Mathematics

41:40 The Long-Term Impact of Lean

The Proof in the Code is out now from Quanta Books. (https://amzn.to/3SuNlJm)

Follow Kevin Hartnett on

X (https://x.com/KSHartnett)

Bluesky (https://bsky.app/profile/kevinhartnett.bsky.social)

Follow Breaking Math on

Substack (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 on

Instagram (https://www.instagram.com/profnoahgian/)

X (https://x.com/ProfNoahGian)

Bluesky (https://bsky.app/profile/profnoahgian.bsky.social)

Follow Autumn on

X (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: [email protected]