OpenAI says its AI cracked Navier-Stokes

We reported September 12 that OpenAI was circling the Millennium Prizes with a new internal model. The World, The Universe And Us now frames the follow-up: OpenAI says it has solved the Navier-Stokes existence and smoothness problem, the 200-year-old question of whether fluid equations can blow up.

The case, as laid out on The World, The Universe And Us, is that the Navier-Stokes equations model flow as a continuous medium, from air over a Formula 1 car to blood through a heart. They were written in the 19th century and underpin modern simulation, but it was open whether smooth three-dimensional flow could stay smooth forever or develop a singularity and produce nonsense.

OpenAI describes the result more precisely. Its proof, produced by an internal system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. The company says the work was done by an internal model that is significantly more capable than GPT-6 Astra, and that it is sharing both a writeup and a formalization in Lean.

Scale is the story. The company ran a system of coordinating agents with tool use and code execution, with the group that produced the Navier-Stokes resolution involving on the order of 10,000 concurrent agents. The agents arrived at the resolution about 88 hours after the first agents were launched, with Lean formalization and verification taking an additional 17 hours via GPT-6 Astra. At a press conference the team said a customer running the same job would pay around $15 million, a figure that arrived after 2.7 million messages and about 130 billion output tokens on Navier-Stokes alone.

That last number is doing a lot of work.

According to The World, The Universe And Us, two researchers had been quietly pushing a stepping-stone version of the problem, the Euler equations, which drop viscosity. Tristan Buckmaster, a mathematician at NYU, and Levent Alpöge, listed as an Anthropic employee, were working with that approach when rumors of progress reached OpenAI. The outlet describes OpenAI then launching efforts on all six open Millennium Problems, later narrowing to Navier-Stokes and Euler, with Buckmaster and Alpöge publishing forced-Euler work the day before OpenAI. The Scientific American account aligns, noting the pair had been using LLMs from OpenAI’s rival company Anthropic to parse through the mathematical possibilities and that the final claim became a credit dispute, not just a proof.

Context matters against what rivals have chosen to showcase. Anthropic recently turned Claude to formal mathematics and produced a computer-checked formalization of Fermat’s Last Theorem, a project that took 11 days of autonomous work. Google DeepMind has taken a different tack with AlphaProof, a reinforcement-learning system that trains itself to prove statements in Lean by first translating informal math into formal statements to build a large library of problems. OpenAI’s Navier-Stokes sprint looks less like a new prover architecture and more like massive orchestration of a general LLM system thrown at an age-old analysis problem, with around 10,000 agents exchanging millions of messages in days.

The skepticism in The World, The Universe And Us is not about the engineering. Mathematician Sébastien Bubeck, who leads OpenAI’s math effort, described having about ten ideas to push past a scaling lull and finding that all of them worked. President Greg Brockman went further and called GPT-6 Astra an early form of artificial general intelligence. The biologists hosting the show pushed back that definitions of AGI remain woolly and that a chatbot that can crush a Millennium-adjacent proof can still fail at simple everyday tasks. Terence Tao, cited by reporter Matt Sparks, put the academic worry bluntly: the system is throwing a carcass of raw meat on the table, not explaining why the theorem holds.

And the why matters for the prize. Scientific American notes the crucial technicality is forcing, an often-ignored term in the Clay formulation that Córdoba and Martínez-Zoroa revived to try to break the equations. Buckmaster and Alpöge used that forcing idea to blow up Euler; OpenAI says it pushed it to full Navier-Stokes. Some mathematicians argue a forced blow-up answers the problem as written but may not answer it as the field intuitively frames it without forcing, which would leave the Clay Mathematics Institute with a quandary over the $1 million award. OpenAI says it does not intend to claim the prize.

The outlet closes the loop by asking where this leaves science. The hosts note chatter that OpenAI may also be aiming at the Hodge conjecture, and that mathematicians worry about role change: applied mathematicians expect to absorb tools like formal Lean checking, while pure theorists sense a nearer-term threat to how proofs are produced. The economics are already stark. If $15 million of compute can compress decades of collective effort into 88 hours, the limiting factor is not whether a model can try every path, but whether the field can still afford to ask why a path is correct.