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

June 24

45 mins

View Transcript

Episode Description

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