Did AI Solve One of Math's Hardest Problems?

A twenty-minute explainer. Tyson asks the astrophysicist Mordecai-Mark Mac Low, who models turbulent gas for a living, what to make of OpenAI’s announcement that AI had settled one of the Millennium Prize problems. The Navier–Stokes equations describe how fluids move. The open question was whether their solutions always stay smooth, or whether some flow could be driven to infinite speed in finite time. OpenAI said its system had found such a blow-up and checked the proof in Lean, a language for machine-verified mathematics.

Mac Low thinks the result is “more likely true than not”. His main point is that it changes nothing for physics. Gas is made of atoms, and the equation for atoms is Boltzmann’s. Chapman and Enskog derived Navier–Stokes from it by assuming that conditions change gently from place to place. A blow-up is exactly where that assumption fails, so the infinity belongs to the approximation and not to any real fluid. Tyson sets it beside Newton: still right where it was tested, and known to be incomplete.

His complaint is about the form. The proof is tens of thousands of machine-checked statements produced by thousands of agents over 88 hours, and “nobody can read that, nobody can build on it.” He contrasts it with two mathematicians, Tristan Buckmaster and Levent Alpöge, who were using AI tools to reach a result they could explain, and who asked OpenAI whether its model had trained on their prompts. He closes on his own use of AI: a literature search tool whose sources are real, though it sometimes gets wrong what they say and who wrote them.

OpenAI’s announcement (8 September 2026) and the 88 hours are as described. The Clay Institute has said the problem “has apparently been settled” and that its process is unhurried, so the prize question is open, and OpenAI says it will not claim it. Several details are off. Lean was created by Leonardo de Moura at Microsoft Research, not at MIT. Buckmaster and Alpöge’s own result is for related equations, with their Navier–Stokes case still being verified, so it is not an independent check of OpenAI’s proof. The $6 million cost and the 26,000 sub-theorems could not be confirmed: Quanta reports “several million dollars”, and one outside count is nearer 36,000. And the prize problem concerns the incompressible equations, a narrower case than the one Mac Low sketches.