On Tuesday, September 8, two important results were announced within hours of each other. NYU mathematician Tristan Buckmaster and Anthropic’s Levent Alpöge posted [1] machine-checked proofs that three sets of fluid equations closely related to Navier-Stokes can break down in finite time, running to infinity from a smooth start and a smooth push. Later that day, OpenAI released [2] a machine-checked proof that Navier-Stokes itself can break down the same way, given a smooth push. That is options C and D of Fefferman’s official problem statement [3], which allows an external force; options A and B, which ask the same question with no force at all, remain open. For context, and to illustrate the difficulty of these problems (I am not a mathmatecian), Navier-Stokes is one of the seven Millennium Prize Problems [3], open for roughly 90 years, with a million-dollar prize attached.
TL;DR
Some of the more important takeaways from the announcement IMO:
The proof came from an unreleased internal model. Not GPT-6 Astra [5], which was announced only days earlier, but an internal model OpenAI describes as significantly more capable, and which is not yet available in ChatGPT or the API.
Eight days from the start of training to a proof. The internal model began training on August 28 and was still training when agents were launched on September 1 [2]. The agents arrived at a proof about 88 hours later, on September 5. Lean verification took another 17 hours, run by GPT-6 Astra. Four days of training produced a frontier-class model with a step-function improvement in capability. Four more days of this model in an agent fleet produced an answer. OpenAI does not say whether that training was a pretraining run or post-training; post-training is the likelier reading.
The method was a parallel search, not one line of reasoning. About 10,000 concurrent agents, split into groups working different variants of the problem statement, seeded by an easier result solved first, with Codex consolidating findings across groups mid-run.
The compute bill runs to millions of dollars. The week-long campaign across all attempted problems consumed about 300 billion output tokens, which TechCrunch puts at roughly $22.5 million [6] at current API rates, though other calculations land nearer $15 million [7], and OpenAI’s own comparison implies less again: earlier math efforts cost about $2,000 in compute and this one was at least a thousand times greater [8]. None of these count input tokens, which OpenAI did not publish.
The output is public and machine-checkable. A 165-page proof and a Lean 4 formalisation anyone can build [12]. OpenAI has said it does not intend to claim the Millennium Prize and frames the release as a report on the pace of AI progress.
In May 2025, about sixteen months ago, I wrote about how AI might impact academic research [9], framed as a thought experiment set in 2027. At the time I worried about how the role of the researcher potentially diminishes, how only teams with the best AI get to participate (this is not good) and how credit/prestige for publishing discoveries might erode. The recent advances on math problems with massive AI agent fleets bring these questions to fore again.
The Multi-Agent Architecture
OpenAI describes the architecture as a system of parallel multi-agent systems [2]: coordinating agents driven by the internal model, with two tools, read access to a cached snapshot of the internet and code execution. Agents were subdivided into groups that could communicate internally, and the Navier-Stokes effort ran on the order of 10,000 concurrent agents.
A parrellel search strategy. Different groups were given different variants of the problem statement, covering all four in Fefferman’s formulation: A and B aiming at global regularity, C and D at breakdown. The groups worked their variants in parallel.
An easier problem was climbed first. About 100 agents spent roughly 50 hours disproving regularity for unforced Euler. That result was then handed to the Navier-Stokes agents as a prompt, so the harder problem started from a foothold rather than from nothing.
Codex was the thing in the middle. It consolidated useful intermediate results and redistributed them across groups. It is the closest thing to an orchestrator that OpenAI describes.
The model improved while the run was going. Mid-effort the agents were switched onto a further-trained checkpoint of the same internal model.
The Navier-Stokes run used 2.7 million messages and about 130 billion output tokens [2]. Divide those:
about 48,000 output tokens per message
about 270 messages per agent, if 10,000 ran throughout
roughly one message every twenty minutes, per agent, across 88 hours
Each message is a long reasoning trace. A reasonable picture here is one of ten thousand slow deliberations running at the same time, each thinking for about twenty minutes at a stretch, with Codex periodically harvesting what worked and passing it back. OpenAI published no breakdown, and 10,000 is its own “on the order of”. GPT-6 Astra then spent another 17 hours formalising and checking the argument in Lean.
Verification and Reproducibility
A good outcome here is that the output of all of this is public. OpenAI released a 165-page analytical proof and a Lean 4 formalisation at github.com/openai/NavierStokesAndEuler [12]. It builds with Lean 4.34.0-rc2 and Mathlib. A successful build here establishes that the proof follows from the definitions as encoded. Whether those definitions and theorem statements faithfully capture the Clay problem is a separate question, and one only mathematicians can settle. The Clay Mathematics Institute has not accepted the result and still lists the problem as unsolved [4] as at time of writing these notes. I would imagine that work is under way.
On reproducibility: While the result is verifiable in this case, the process that led to it is not particularly reproducible. OpenAI does not say how many sub groups of agents there were or how large, what a single agent’s loop looks like, how candidate results were scored or selected, or how the 165-page manuscript was assembled from group output.
What Changes for Researchers
Reflecting on these advances and the state of progress, it is clear that the way research is conducted will change has changed, and in more ways than I explored in my previous article [9]. It raises more questions than answers.
If compute is tied to research outcomes, that narrows the pool of who can participate. Compute here means two things: access to the best frontier models, and access to enough compute to run inference in parallel at speed/scale. This result needed both. An internal model still in training did the reasoning, and about 10,000 concurrent agents did the searching, for a bill in the millions. Buckmaster and Alpöge had worked their program for about a year, with most of the results arriving in the final month, and that year already had heavy LLM assistance in it [1]. Where those two things decide who reaches a result first, the set of people who can reach it at all gets smaller.
Ofcourse, there is always the legit argument that the cost of inference will fall over time, and indeed it has. However, observations in recent years suggest that the cost of truly frontier models has not.
There are new rules of engagement around the tools of research. Tools used to be tools. A telescope, a solver, a compiler: none of them learned anything from being pointed at your problem. That is no longer true. OpenAI’s announcement states that while no specific user data was accessed, it cannot rule out that de-identified data from the use of its products helped improve its models [2]. So there is a question now that did not exist before: as I use a tool, how do I get the benefit of it without giving up my IP and my work? This is a difficult question. Organizations have grappled with it for years as a matter of IP protection, with legal teams and negotiated terms behind them. Individual academics have neither, and have important new decisions to navigate here.
