DEV Community

Cover image for Navier-Stokes solved? What OpenAI's proof shows and why it's disputed
Nikoloz Turazashvili (@axrisi)
Nikoloz Turazashvili (@axrisi) Subscriber

Posted on

Navier-Stokes solved? What OpenAI's proof shows and why it's disputed

#openai #ai #math #anthropic

On September 8, 2026, OpenAI published a proof that the Navier-Stokes equations can blow up: a smooth 3D fluid, pushed by a smooth force, can reach infinite velocity in finite time. That would settle a Clay Millennium Prize problem open for about 90 years, and an internal model found it as roughly 10,000 agents running for 88 hours. Twelve hours earlier, an NYU professor had posted a statement saying OpenAI started the run after hearing about his own work on the same problem. For developers there is a second story: the professors had been putting their drafts into Codex for a year, and OpenAI's post has a footnote about it.

TL;DR

  • OpenAI says an internal model, "significantly more capable than GPT-6 Astra", produced a proof and a Lean formalization that settles statements C and D of the Clay Navier-Stokes problem: smoothness fails (OpenAI).
  • The Navier-Stokes run used on the order of 10,000 concurrent agents, 2.7 million messages and about 130 billion output tokens. At GPT-6 Astra list prices, roughly $6.5 million, for a $1 million prize OpenAI says it will not claim.
  • NYU's Tristan Buckmaster and Anthropic's Levent Alpöge reached Euler blow-up on August 15, using Claude and Codex. Buckmaster's statement says OpenAI's first prompt came "after information about our work had reached OpenAI".
  • OpenAI says nobody looked at their work or user data, but "we cannot rule out that de-identified data derived from their usage of our products helped improve our models."

What is the Navier-Stokes Millennium Prize problem?

The Navier-Stokes equations describe how an incompressible fluid moves. In the standard form, with velocity u, pressure p, viscosity ν and an applied force f:

∂u/∂t + (u · ∇)u = −∇p + νΔu + f
∇ · u = 0
Enter fullscreen mode Exit fullscreen mode

The open question, going back to Jean Leray in 1934, is whether a solution that starts smooth in three dimensions always stays smooth, or whether it can develop a singularity: a point where the velocity goes to infinity in finite time. Since 2000 it has been one of Clay's seven Millennium Prize problems, $1 million each. The Clay formulation has four statements; A and B say smooth solutions always exist, C and D say they can break down. OpenAI claims C and D: a disproof of smoothness.

What OpenAI's Navier-Stokes proof claims

From OpenAI's post: start with a fluid at rest, apply a smooth force, keep the total energy finite, and the solution develops a vortex that "spirals inward and gets increasingly elongated, like spaghetti" until the velocity is infinite. The proof and Lean code are on GitHub; formalizing and verifying took 17 hours with GPT-6 Astra.

Lean is a proof assistant: a language whose compiler checks every step of a proof. If the statement is formalized correctly and the file compiles, the proof holds, whoever or whatever wrote it. A toy example (illustrative, not from OpenAI's repo):

-- the type is the claim, the term after := is the proof; the compiler checks it
theorem add_zero_example (n : Nat) : n + 0 = n := rfl
Enter fullscreen mode Exit fullscreen mode

So the open questions are about process, not correctness.

How OpenAI ran 10,000 agents for 88 hours

Per OpenAI, the internal model began training on August 28. On Tuesday, September 1, "we heard rumors that two Millennium Prize problems had been resolved", so OpenAI pointed it at every open Millennium problem. The Navier-Stokes group ran on the order of 10,000 concurrent agents with a cached internet and code execution, with Codex consolidating insights between groups. They did the easier unforced Euler problem first (about 100 agents, about 50 hours) and reached Navier-Stokes on Saturday, September 5, about 88 hours after launch.

Messages Output tokens Rough cost at Astra list price ($50 per 1M output)
Navier-Stokes group 2.7 million ~130 billion ~$6.5 million
All Millennium problems 4.9 million ~300 billion ~$15 million

The cost column is my arithmetic. The internal model has no public price, so these are GPT-6 Astra list prices, not OpenAI's bill. The top Hacker News comment: "Don't even try to do the math on how much that would cost at normal API prices."

The dispute: Buckmaster and Alpöge's statement

Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic, collaborating personally) had spent a year on a program opened by Diego Córdoba and Luis Martínez-Zoroa. They used Claude and Codex, and Buckmaster writes: "I pay for the tools my group uses out of my own research funds, including footing a large bill to OpenAI."

His four-page statement, posted September 8 at 05:42 UTC, was number one on Hacker News all day, with 1,683 points. The timeline it gives:

Date Event (per Buckmaster's statement unless noted)
Aug 15 Blow-up with smooth forcing for Boussinesq and 3D Euler. The first LLM proof is "the most horrendous I have ever read".
Aug 22 Euler result verified in Lean
Sep 1 OpenAI hears the rumor and starts its run (per OpenAI)
Sep 3 Buckmaster emails a prominent mathematician at OpenAI. Same-day reply: "it would be useful to avoid competing here… happy to provide compute"
Sep 6, 12:45 OpenAI asks to meet "at any point today". Sébastien Bubeck joins; two calls
Sep 8 Statement posted at dawn; OpenAI's post that afternoon

On the call, he writes, he was told the model produced the forced Navier-Stokes blow-up with "very little human input". "This turned out not to be true": there was an entire team, easier problems first, a prompt written by prompting Codex, and "an insane amount of compute". Asked when the first prompt was sent, the answer was "in the past few days, after information about our work had reached OpenAI".

Two offers followed: they post Euler and OpenAI posts Navier-Stokes the next day, or Buckmaster alone writes up the Navier-Stokes paper, acknowledging the OpenAI model. He writes that "Sebastien twice asserted that he wanted Levent removed from authorship", and quotes two lines from the call: "Why would you ruin your career?" and "If you don't want me to be nice, then I don't have to be nice."

He is careful: "I have not seen OpenAI's proof… I am not accusing anyone of anything."

A third group (Ganeshram, Duruisseaux, Anandkumar) posted an independent Euler blow-up the same weekend.

OpenAI's side, and the footnote about Codex data

OpenAI's post and its post on X say: "We (the researchers and the agents) did not see any of their work", and no specific user data was accessed. Then: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models."

Alpöge quoted that line: "i mean props to them for straight coming clean." Mark Chen of OpenAI answered the data question directly: "Did any human or agent look at user data as part of the Navier Stokes effort? No. Do we use user feedback and de-identified data to improve ChatGPT and Codex in a holistic way? Yes."

Bubeck wrote: "I never ever asked for Levent to be removed from authorship of his own work." Sam Altman posted that "Seb--and everyone else--acted with integrity and generosity throughout", that "we felt it was challenging to offer the same to Levent (an Anthropic employee)", and that "the team threatened us with unfounded accusations of plagarism [sic]". His reason for the run: "there were rumors on the internet last week that Anthropic's models had solved a millennium problem and we were curious if ours could do it too."

Both sides agree OpenAI heard a rumor and reached a result in days. They disagree on what was said on the calls.

The developer lesson is in Chen's answer, not in the math. Put unpublished work into a hosted coding assistant and the vendor's position may be: nobody looks at your sessions, and de-identified usage data still improves the models. Read your plan's data terms and check whether training is opted out for your organisation.

Terence Tao on AI and open problems

Terence Tao called the Alpöge-Buckmaster result "A remarkable achievement" and noted that Buckmaster "kindly explained some of the key ideas to me over the phone, which made a refreshing change from AI-based communication modalities."

That evening he posted a four-part thread, the part of this story that will outlast it: Open problems are now "mined in a non-renewable fashion", and "it is now the identification of a promising problem which is the scarce and precious resource." Then: "We have now seen that even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it before the original research project has time to reach its full potential." The incentive may now point toward "no longer sharing any promising research directions", which would "reverse centuries of traditions of open science". (HN)

The same applies to anyone who works in the open: a public roadmap or a preprint is now a signal a well-funded lab can act on within a weekend.

Also today: an Anthropic resignation and Meta Muse

Jacob Coxon resigned from Anthropic. His post, 43.9 million views: "I spent the last three years doing pretraining research at both OpenAI and Anthropic. Neither company is acting responsibly. They are racing straight to self-improving superintelligence and gambling with our lives." (HN)

Meta shipped Muse, a personal AI agent that runs on its own cloud VM with its own browser. You talk to it in WhatsApp; a separate Sentinel agent approves anything that reaches the internet. US only. Top HN comment: "I really don't want to share all my personal life information with meta like this." (HN)

Verdict: NEEDS REVIEW

I stamped it NEEDS REVIEW. The proof compiles; the story doesn't. Ten thousand agents closing a 90-year-old problem in a weekend is the capability result of the year. Announcing it after a Sunday call to the two people you heard the rumor about, with a footnote about their Codex usage, is not.

FAQ

Has the Navier-Stokes problem been solved?
OpenAI says its proof, formalized in Lean, resolves statements C and D of the Clay formulation by showing a smooth solution can blow up. OpenAI says it will not claim the $1 million prize.

Did OpenAI use Buckmaster and Alpöge's work?
OpenAI says no researcher or agent saw their work and no specific user data was accessed, but it "cannot rule out" that de-identified data from their product use helped improve its models. Buckmaster says he is not accusing anyone.

What did Terence Tao say about AI and math?
That open problems are now "mined in a non-renewable fashion", and that a rumor alone can trigger an AI effort to flatten one.

Sources

This article expands on an episode of **The Daily Diff, a five-minute daily video on what shipped and what broke in tech.
Watch the episode · Subscribe on YouTube · the written diff lands in your inbox every morning at thedailydiff.dev.

Top comments (1)