OpenAI says AI has settled Navier–Stokes. The dispute that followed matters too

On 8 September 2026, OpenAI announced that an unreleased internal system had proved that the three-dimensional Navier–Stokes equations can break down in finite time. If it holds, one of the seven Millennium Prize Problems has been settled by a machine. It arrived wrapped in a credit dispute that says as much about AI research as about mathematics.

The claim

According to OpenAI, an internal multi-agent system, described as "significantly more capable than GPT-6 Astra", produced a proof that smooth solutions of the incompressible Navier–Stokes equations in three dimensions, driven by a smooth external force, can develop a singularity: the velocity becomes infinite in finite time. The run began on 1 September and lasted 88 hours. It used more than 10,000 agents, exchanged some 2.7 million messages and generated around 130 billion output tokens. The output was a 166-page paper accompanied by a formalisation in the Lean proof assistant [OpenAI, 2026; Wikipedia, 2026].

The Clay Mathematics Institute's official problem statement, written by Charles Fefferman, can be resolved in either direction, and one of the accepted forms of a negative answer is exactly this: a breakdown of smooth solutions on all of three-dimensional space with a smooth forcing term. On 11 September the Institute said that the problem "has apparently been settled", while stressing that its own verification would be "deliberately unhurried" [Wikipedia, 2026]. Fefferman himself told Quanta he was thrilled the problem had been solved, while naming the human mathematicians whose earlier work made it possible as "the heroes of the story" [Quanta, 2026].

What the Lean formalisation does and does not settle

The formal proof is the most important part of the claim. Lean checks every step of a proof against a small trusted kernel, so a proof that type-checks has no gaps or skipped steps. That is a far stronger guarantee than a 166-page manuscript read by referees.

It is not the end of the matter. Humans still have to confirm that the statement proved in Lean is logically equivalent to the statement mathematicians care about: that the formal definitions of "smooth solution", "forcing" and "blow-up" match the standard ones, with no subtle loophole. The proof also relies on Mathlib, a large community library whose definitions have to be trusted too. This is why a machine-checked proof can still take months of human scrutiny, and why the Institute is not hurrying [Quanta, 2026].

The credit dispute

The result did not come out of nowhere. On 15 August, the mathematicians Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic), working with Anthropic models, proved that the Euler equations, the frictionless cousin of Navier–Stokes, can blow up under smooth forcing. They verified that result in Lean a week later. Their work, and the approach of Diego Córdoba and Luis Martínez-Zoroa before them, is the direct lineage of the Navier–Stokes result [TechCrunch, 2026; Quanta, 2026].

On the night of 7 September, roughly twelve hours before OpenAI's announcement, Buckmaster published a statement alleging that their unpublished advances had been passed to OpenAI days earlier and may have shaped the prompts given to OpenAI's agents. OpenAI denied it. Sébastien Bubeck said the company "did not use their prompts or proofs" and had not seen the work before it was made public. OpenAI's account shifted over the following days, from acknowledging that de-identified usage data could have helped improve its models, to saying it was "categorically" impossible that Buckmaster's prompts had influenced the system, to asserting on 13 September that no user input after 3 July could have affected the work [Wikipedia, 2026]. Buckmaster also alleged that Bubeck had told him Alpöge's name should be removed from any joint publication because of his Anthropic affiliation [TechCrunch, 2026].

We are not in a position to adjudicate the leak allegation, and it may never be resolved to everyone's satisfaction. What is not in dispute is that the AI system's result sits on top of years of human work, a point Fefferman, Córdoba and Buckmaster have all made in public.

The reaction from mathematics

The response from the mathematical community has been less celebratory than the headlines. On 11 September, 26 Fields Medallists published an open letter titled "A Severe Misalignment of AI in Mathematics", warning that the discipline's values of conceptual understanding and insight risk erosion when problems are attacked by industrial-scale search. Terence Tao criticised the practice of announcing results through press releases and social media rather than academic channels, and worried that the race could discourage mathematicians from working independently [Wikipedia, 2026]. Buckmaster, for his part, has since called the scramble for papers and credit "pointless".

There is also the question of what a proof is for. Buckmaster described the first machine-generated proof he saw as "the most horrendous" he had ever read. A proof that is correct but unreadable settles a question without necessarily explaining it, and explanation is much of what mathematicians value.

Why this matters beyond mathematics

For AI safety and governance, three things stand out.

Scale changes the nature of the work. Ten thousand agents running for nearly four days is not an assistant helping a mathematician. It is an organisation, and it produced a result that no individual could have checked without the formal proof. As systems do more of the work, verification becomes the scarce resource, which is precisely where formal methods earn their keep.

Attribution norms are not ready. Authorship conventions assume identifiable human contributors. They say nothing about a system that may have been influenced, directly or through usage data, by other people's unpublished work. The same question will arise in science, law and software, wherever AI systems learn from the work of the people using them.

Capability claims are arriving faster than the checks. The Navier–Stokes run came in the same weeks as OpenAI's agent-containment incidents and Anthropic's call to pace the frontier. A system that can organise ten thousand agents to settle a century-old problem is also a system whose behaviour at scale needs oversight that works. The mathematics community's instinct to slow down, verify and argue about credit is not obstruction. It is the kind of scrutiny the rest of the field could use more of.

References

Axios (2026). "OpenAI's historic math solution overshadowed by credit controversy." 8 September. axios.com.

Clay Mathematics Institute. "Navier–Stokes Equation." Official problem description by C. Fefferman. claymath.org.

OpenAI (2026). Announcement of a proposed Navier–Stokes solution, 8 September.

Quanta Magazine (2026). "AI Has Solved One of Math's $1 Million Millennium Prize Problems." 8 September. quantamagazine.org.

Scientific American (2026). "OpenAI claims blockbuster math breakthrough amid swirl of controversy." scientificamerican.com.

TechCrunch (2026). "OpenAI fought dirty on career-making math problem, says NYU mathematician." 8 September. techcrunch.com.

Wikipedia (2026). "Navier–Stokes priority controversy." Accessed 27 September 2026. wikipedia.org.