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 problem1:50 Kepler's oranges and the proof nobody could check6:54 How mathematicians decide a proof is true9:04 Correct is not the same as useful12:17 Sponsor: Cyber Fund12:53 What Lean is, and the small kernel it trusts15:23 From Microsoft's Z3 to Lean18:22 The argument over Lean's foundations24:52 One researcher versus a growing user base26:16 Kevin Buzzard's house of cards30:43 Mathlib as a barn raising37:16 The perfectoid-spaces stunt47:12 Scholze's proof nobody had read: Liquid Tensor53:20 Can AI learn to find proofs? AlphaProof58:43 AI mathematics in 2026 and Tao's experiment1:01:36 Lean's place in AI mathematics1:02:17 AI brute force versus the right abstraction1:05:19 Autoformalisation's Trojan horse1:07:25 The formalisation gap1:11:45 A proof is not understanding1:16:58 Integration hell and the zlib specification1:21:14 Verification in the AI software lifecycle1:22:38 The human story behind Lean1:31:09 The birthday walk1: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] Leanhttps://lean-lang.org/[30:43] Mathlibhttps://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 Experimenthttps://github.com/leanprover-community/lean-liquid[53:20] AlphaProof (Google DeepMind): AI achieves silver-medal standard solving International Mathematical Olympiad problemshttps://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-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
Chapters
Read the transcript
https://app.rescript.info/public/share/cOKcz4pWRPjh7BTIgybd7PUr_vChUaY6VQW64No8XMs
Aug 14, 2025 01:45:39
DeepMind Genie 3 [World Exclusive] (Jack Parker Holder, Shlomi Fruchter)
This episode features Shlomi Fuchter and Jack Parker Holder from Google DeepMind, who are unveiling a new AI called Genie 3. The host, Tim Scarfe, describes it as the most mind-blowing technology he has ever seen. We were invited to their offices to conduct the interview (not sponsored).Imagine you could create a video game world just by describing it. That's what Genie 3 does. It's an AI "world model" that learns how the real world works by watching massive amounts of video. Unlike a normal video game engine (like Unreal or the one for Doom) that needs to be programmed manually, Genie generates a realistic, interactive, 3D world from a simple text prompt.**SPONSOR MESSAGES***Prolific: Quality data. From real people. For faster breakthroughs.https://prolific.com/mlst?utm_campaign=98404559-MLST&utm_source=youtube&utm_medium=podcast&utm_content=script-gen***Here’s a breakdown of what makes it so revolutionary:From Text to a Virtual World: You can type "a drone flying by a beautiful lake" or "a ski slope," and Genie 3 creates that world for you in about three seconds. You can then navigate and interact with it in real-time.It's Consistent: The worlds it creates have a reliable memory. If you look away from an object and then look back, it will still be there, just as it was. The guests explain that this consistency isn't explicitly programmed in; it's a surprising, "emergent" capability of the powerful AI model.A Huge Leap Forward: The previous version, Genie 2, was a major step, but it wasn't fast enough for real-time interaction and was much lower resolution. Genie 3 is 720p, interactive, and photorealistic, running smoothly for several minutes at a time.The Killer App - Training Robots: Beyond entertainment, the team sees Genie 3 as a game-changer for training AI. Instead of training a self-driving car or a robot in the real world (which is slow and dangerous), you can create infinite simulations. You can even prompt rare events to happen, like a deer running across the road, to teach an AI how to handle unexpected situations safely.The Future of Entertainment: this could lead to a "YouTube version 2" or a new form of VR, where users can create and explore endless, interconnected worlds together, like the experience machine from philosophy.While the technology is still a research prototype and not yet available to the public, it represents a monumental step towards creating true artificial worlds from the ground up.Jack Parker Holder [Research Scientist at Google DeepMind in the Open-Endedness Team]https://jparkerholder.github.io/Shlomi Fruchter [Research Director, Google DeepMind]https://shlomifruchter.github.io/TOC:[00:00:00] - Introduction: "The Most Mind-Blowing Technology I've Ever Seen"[00:02:30] - The Evolution from Genie 1 to Genie 2[00:04:30] - Enter Genie 3: Photorealistic, Interactive Worlds from Text[00:07:00] - Promptable World Events & Training Self-Driving Cars[00:14:21] - Guest Introductions: Shlomi Fuchter & Jack Parker Holder[00:15:08] - Core Concepts: What is a "World Model"?[00:19:30] - The Challenge of Consistency in a Generated World[00:21:15] - Context: The Neural Network Doom Simulation[00:25:25] - How Do You Measure the Quality of a World Model?[00:28:09] - The Vision: Using Genie to Train Advanced Robots[00:32:21] - Open-Endedness: Human Skill and Prompting Creativity[00:38:15] - The Future: Is This the Next YouTube or VR?[00:42:18] - The Next Step: Multi-Agent Simulations[00:52:51] - Limitations: Thinking, Computation, and the Sim-to-Real Gap[00:58:07] - Conclusion & The Future of Game EnginesREFS:World Models [David Ha, Jürgen Schmidhuber]https://arxiv.org/abs/1803.10122POEThttps://arxiv.org/abs/1901.01753[Akarsh Kumar, Jeff Clune, Joel Lehman, Kenneth O. Stanley]The Fractured Entangled Representation Hypothesishttps://arxiv.org/pdf/2505.11581TRANSCRIPT:https://app.rescript.info/public/share/Zk5tZXk6mb06yYOFh6nSja7Lg6_qZkgkuXQ-kl5AJqM
Aug 05, 2025 58:23
Show more episodes
© 2026 Spotify AB Careers Legal Help
App Store Google Play