Mathematics Just Changed Forever — Kevin Hartnett
Kevin Hartnett is the author of *The Proof in the Code*. SPONSOR: --- Cyber Fund built the Monastery to help founders ship products that were impossible a year ago. Applications for Batch 1 are now open. Apply now: https://cyber.fund --- In 1998 Thomas Hales finished a proof of the Kepler conjecture that leaned so heavily on computer code that the Annals of Mathematics could not say whether it was true. That impasse opens Kevin Hartnett's book *The Proof in the Code*, and this documentary. Built around Tim's conversation with Hartnett, the film follows Lean from a side project at Microsoft Research to the system mathematicians now use to check their own field. Leonardo de Moura, Lean's creator, explains why everything rests on a small trusted kernel. Jeremy Avigad recalls the argument over foundations that changed Lean. Kevin Buzzard describes his fear that his corner of mathematics was becoming a house of cards, and Paul Lessard separates a correct proof from a useful one. Mathlib, Peter Scholze's Liquid Tensor challenge and Terence Tao's Equational Theories project all pass through. The second half turns to AI. AlphaProof, natural-language olympiad proofs and autoformalisation sharpen the question the book keeps asking: when a machine produces a proof nobody can read, what has actually been checked? The answer lies in the formalisation gap, the distance between the mathematics people mean and the statement a checker certifies. The film closes on the human story behind the software. --- TIMESTAMPS: 0:00 Cold open: proof, code and the wrong problem 1:50 Kepler's oranges and the proof nobody could check 6:54 How mathematicians decide a proof is true 9:04 Correct is not the same as useful 12:17 Sponsor: Cyber Fund 12:53 What Lean is, and the small kernel it trusts 15:23 From Microsoft's Z3 to Lean 18:22 The argument over Lean's foundations 24:52 One researcher versus a growing user base 26:16 Kevin Buzzard's house of cards 30:43 Mathlib as a barn raising 37:16 The perfectoid-spaces stunt 47:12 Scholze's proof nobody had read: Liquid Tensor 53:20 Can AI learn to find proofs? AlphaProof 58:43 AI mathematics in 2026 and Tao's experiment 1:01:36 Lean's place in AI mathematics 1:02:17 AI brute force versus the right abstraction 1:05:19 Autoformalisation's Trojan horse 1:07:25 The formalisation gap 1:11:45 A proof is not understanding 1:16:58 Integration hell and the zlib specification 1:21:14 Verification in the AI software lifecycle 1:22:38 The human story behind Lean 1:31:09 The birthday walk 1:33:05 Farewell --- REFERENCES: [2:12] Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005) https://annals.math.princeton.edu/2005/162-3/p01 [2:12] The Flyspeck project (the formal proof of the Kepler conjecture) https://github.com/flyspeck/flyspeck [12:53] Lean https://lean-lang.org/ [30:43] Mathlib https://github.com/leanprover-community/mathlib4 [30:43] Kevin Hartnett, "Building the Mathematical Library of the Future" (Quanta Magazine, 2020) https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ [47:12] The Liquid Tensor Experiment https://github.com/leanprover-community/lean-liquid [53:20] AlphaProof (Google DeepMind): AI achieves silver-medal standard solving International Mathematical Olympiad problems https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/ [59:23] The Equational Theories Project (Terence Tao) https://github.com/teorth/equational_theories [1:18:30] lean-zip (the zlib proof) https://github.com/kim-em/lean-zip FrontierMath Erdős (Epoch AI, 2026) https://epoch.ai/benchmarks/frontiermath-erdos Book: Kevin Hartnett, *The Proof in the Code* (Quanta Books, 2026) https://www.quantabooks.org/books/the-proof-in-the-code/ Image credits: photo of Peter Scholze by George Bergman (Oberwolfach Photo Collection), GFDL 1.2, https://commons.wikimedia.org/wiki/File:Peter_Scholze.jpg (licence: https://www.gnu.org/licenses/old-licenses/fdl-1.2.html) --- RESCRIPT: https://app.rescript.info/share/8604a0cd6ea4604a368028a05f4e6be4 Support MLST on Patreon: https://www.patreon.com/mlst Discord: https://discord.gg/HNnAwSduud
