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