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 Ensur ...