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: Cold open: proof, code and the wrong problem Kepler's oranges and the proof nobody could check How mathematicians decide a proof is true Correct is not the same as useful Sponsor: Cyber Fund What Lean is, and the small kernel it trusts From Microsoft's Z3 to Lean The argument over Lean's foundations One researcher versus a growing user base Kevin Buzzard's house of cards Mathlib as a barn raising The perfectoid-spaces stunt Scholze's proof nobody had read: Liquid Tensor Can AI learn to find proofs? AlphaProof AI mathematics in 2026 and Tao's experiment Lean's place in AI mathematics AI brute force versus the right abstraction Autoformalisation's Trojan horse The formalisation gap A proof is not understanding Integration hell and the zlib specification Verification in the AI software lifecycle The human story behind Lean The birthday walk Farewell---REFERENCES:[] Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005)https://annals.math.princeton.edu/2005/162-3/p01[] The Flyspeck project (the formal proof of the Kepler conjecture)https://github.com/flyspeck/flyspeck[] Leanhttps://lean-lang.org/[] Mathlibhttps://github.com/leanprover-community/mathlib4[] Kevin Hartnett, "Building the Mathematical Library of the Future" (Quanta Magazine, 2020)https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/[] The Liquid Tensor Experimenthttps://github.com/leanprover-community/lean-liquid[] AlphaProof (Google DeepMind): AI achieves silver-medal standard solving International Mathematical Olympiad problemshttps://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/[] The Equational Theories Project (Terence Tao)https://github.com/teorth/equational_theories[] lean-zip (the zlib proof)https://github.com/kim-em/lean-zipFrontierMath Erdős (Epoch AI, 2026)https://epoch.ai/benchmarks/frontiermath-erdosBook: Kevin Hartnett, *The Proof in the Code* (Quanta Books, 2026)https://www.quantabooks.org/books/the-proof-in-the-code/---RESCRIPT: https://app.rescript.info/share/8604a0cd6ea4604a368028a05f4e6be4Support MLST on Patreon: https://www.patreon.com/mlstDiscord: https://discord.gg/HNnAwSduud
