OpenAI just dropped a paper claiming a full solution to the Navier-Stokes existence and smoothness problem. It is one of the seven Clay Millennium Prize problems, open for 92 years since Jean Leray's 1934 paper.
They proved finite-time blowup: an initially smooth 3D incompressible fluid develops an infinite velocity singularity in finite time while keeping total energy finite. The blowup mechanism is a thinning vortex spiral stretched axially like spaghetti, where acceleration, pressure gradients, and viscosity balance out (I don't understand any of it, but apparently the math equations break down and the fluid moves infinitely fast, lol).
They verified the whole proof in Lean. The formalization is public on GitHub.
The Model
OpenAI did not use GPT-6 Astra for the mathematical discovery. They used an unreleased internal frontier model trained since Aug 28 that people are calling GPT-7. As shown in the chart above, the internal model delivers 2-3x Astra's performance across the board.
Astra was only brought in at the tail end as a verification worker to convert the math into Lean code.
The 10,000 Agent Swarm
The compute scale is wild:
- 10,000 concurrent agents communicating in sub-swarms.
- 2.7 million agent messages.
- 130 billion output tokens burned on Navier-Stokes alone.
- 300 billion output tokens across all attempted problems ($22.5 million worth of compute at current Astra pricing).
- Codex was used to cross-pollinate intermediate lemmas between competing agent clusters.
The run finished in 88 hours. The Lean formalization took another 17 hours.
The Timeline
(Sept 1) Rumors circulate in London and tech circles that Anthropic researcher Levent Alpöge and NYU math professor Tristan Buckmaster resolved a major open problem. OpenAI thinks it is Navier-Stokes, panics, and launches 10,000 agents across every open Millennium problem.
(Sept 3) 100 agents solve unforced Euler regularity in 50 hours. OpenAI realizes fluid mechanics is their best shot and shifts all compute to Navier-Stokes.
(Sept 5) The agent swarm finds the Navier-Stokes blowup proof.
(Sept 6) Astra finishes the Lean verification. OpenAI reaches out to Anthropic and Buckmaster to offer a joint announcement, only to realize the Anthropic team had actually worked on forced Euler, not Navier-Stokes.
(Sept 8) OpenAI publishes the Navier-Stokes paper and Lean repo. They are not claiming the $1M Clay prize.
The Codex Controversy
Right after the release, the math community exploded when Tristan Buckmaster published a four-page statement detailing what actually happened behind the scenes.
Buckmaster and Alpöge had spent over a year working quietly on fluid blowup. Their entire effort was built on a mathematical program started by Diego Córdoba and Luis Martínez-Zoroa (Buckmaster notes in his statement that Martínez-Zoroa deserves a Fields Medal for it).
Because it was an independent collaboration, Buckmaster paid for their tools out of his university research budget, running drafts, lemmas, and scratchpad calculations through OpenAI Codex sessions for months.
On Sunday (Sept 6), OpenAI researcher Sébastien Bubeck got on a call with Buckmaster. Bubeck claimed OpenAI's model had found a 100-page proof of forced Navier-Stokes blowup using "very little human input."
Buckmaster immediately smelled smoke. The proof followed the exact route through smooth forcing (options c and d in Charles Fefferman's official Clay problem statement) that Córdoba, Martínez-Zoroa, and Buckmaster had spent years developing. Almost nobody else in the world was working on that specific attack angle. It is not something an AI stumbles on in four days from a cold prompt.
On the call, OpenAI's story started shifting as engineers sent live corrections over internal chat:
- The first prompt had only been sent a few days earlier, right after rumors of Buckmaster's progress reached OpenAI.
- Even the prompt fed to the model had been generated by Codex.
- When Buckmaster asked if OpenAI had trained on or accessed their private Codex drafts, OpenAI said the model didn't look up user data. When he pressed on training data, they went completely silent.
Then came the corporate pressure.
Bubeck offered two deals: either Buckmaster posts Euler first and OpenAI posts Navier-Stokes the next day, or Buckmaster alone writes the paper with OpenAI's model. Bubeck twice insisted on cutting Levent Alpöge out of authorship entirely because he works at Anthropic.
When Buckmaster refused and said he would go public, Bubeck fired back:
> "Why would you ruin your career?"
When Buckmaster replied that he was an academic and asked why going public would ruin him, Bubeck said:
> "If you don't want me to be nice, then I don't have to be nice."
Bubeck then texted Alpöge behind Buckmaster's back, asking for a 1-on-1 and saying: "I don't know if Tristan is being fully rational right now." Alpöge refused.
Bubeck has since publicly called the allegations "false and inflammatory," promising a formal reply. But OpenAI's own published blog post included this quiet sentence:
> "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models."
They also openly stated they used Codex to synthesize and cross-pollinate intermediate reasoning steps between their 10,000 agents.
Now the entire math community is debating the brutal new reality of brute-force AI: did OpenAI discover a solution to a 90-year-old problem, or did a $22.5 million swarm of 10,000 agents brute-force the finish line using clues leaked from a researcher's private cloud scratchpad?
If you are working on a Millennium Prize problem, use an open LLM or self-hosted, lol.