Did AI Solve One of Math’s Hardest Problems?

Summary
Astrophysicist Neil deGrasse Tyson and colleague Mordecai-Mark Mac Low discuss OpenAI's claim of finding a finite-time blowup singularity in the Navier–Stokes equations, one of the Clay Mathematics Institute's Millennium Prize Problems. They explore fluid dynamics, the mechanics of turbulence, the contrast between continuous fluid equations and particle-based physics (the Boltzmann equation), and the broader implications of AI-generated formal mathematical proofs versus human conceptual understanding.

What is shown

• [00:02] Headline from ScienceNews: "AI may have solved one of math's biggest puzzles, raising controversy".
• [00:15] Visual simulations and diagrams illustrating fluid flow over aircraft wings, volcanic lava, and turbulent air currents.
• [03:22] Diagram and 3D animation explaining how golf ball dimples induce boundary-layer turbulence to reduce overall aerodynamic drag.
• [03:41] Presentation of the Navier–Stokes equations and portraits of Claude-Louis Navier and Sir George Stokes.
• [07:20] Screenshot of OpenAI's announcement claiming an internal AI system produced a proof showing Navier–Stokes dynamics can develop a finite-time singularity, formalized in Lean.
• [08:11] Display of thousands of lines of Lean proof code.
• [08:36] BBC/Reuters headline: "OpenAI says it cracked 90-year-old maths problem in 88 hours" with details on the compute used.
• [08:56] Profiles of mathematicians Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic) concerning parallel work and priority/data attribution disputes.
• [10:48] Breakdown of the Boltzmann equation and visual simulations of discrete particle/molecular collisions in gas versus continuous fluid models.
• [20:40] Tyson presents his co-authored book Lost in Space.

Claims & numbers

• Mac Low states that OpenAI's proof was produced using a swarm of roughly 10,000 AI agents running on approximately $6 million worth of GPUs across 88 hours [08:38].
• Mac Low notes the Lean formalization of the Navier–Stokes counterexample proof comprises around 26,000 subtheorems [10:08].
• The presenters note the Millennium Prize Problems carry a $1 million award per solved problem [07:31].
• Mac Low describes using AI literature tools in his research, stating the tool reliably retrieves authentic paper citations but still occasionally hallucinates author attribution [18:42, 19:18].

Notable quotes

• [02:51] Mordecai-Mark Mac Low: "Turbulence is."
• [09:07] Mordecai-Mark Mac Low: "We have a solution that we have been translating out of AI slop into human-readable format..."
• [17:17] Mordecai-Mark Mac Low: "The problem with the OpenAI solution is that wasn't unpacked... they produced a solution, they provided this immense package of Lean statements, but nobody can read that. Nobody can build on it."

Assessment
This is a discussion and commentary video from StarTalk analyzing OpenAI's September 2026 Navier–Stokes singularity announcement and related academic reaction. While the hosts clearly explain the underlying fluid dynamics and mathematical history, neither host ran or independently verified the 26,000-subtheorem Lean codebase themselves during the segment.

Described by gemini-3.8-flash on 2026-10-05 from the video's audio and frames.