OpenAI claims that an internal system, presented as markedly more capable than GPT-6 Astra, produced a solution to the Navier-Stokes problem. Around 10,000 coordinated agents are said to have worked for 88 hours before succeeding. A proof formalised in Lean has been published. Nothing has been validated at this stage. It is independent mathematicians who will determine whether the result holds, and that will take weeks or months. We are reporting an announcement, not an established fact.
Yesterday we covered a proof concerning the Euler equations obtained with models and formally verified. Here is the escalation, and it arrives with a complication.
What this is about
The Navier-Stokes equations describe the flow of viscous fluids: the air around a wing, water in a pipe, blood in an artery. They work remarkably well in practice, and nobody knows how to demonstrate that they always behave correctly.
The open question is that of existence and smoothness: do solutions remain well defined forever, or can they become infinite in finite time? The latter case is called a singularity, or blow-up.
It is one of the seven millennium problems posed in 2000, each carrying a prize of one million dollars. Only one has been solved since.
According to OpenAI, the proof produced establishes that a three-dimensional fluid governed by these equations can develop a singularity in finite time. It is the direct continuation of the work on Euler that we reported yesterday, with an extra degree of difficulty: Navier-Stokes adds viscosity, which tends to smooth solutions and makes blow-up much harder to obtain.
What makes the announcement serious
One point sets it apart from previous claims, and it is the one we highlighted yesterday as decisive: a proof formalised in Lean has been published.
We explained this in our article on formal verification: a proof assistant mechanically checks every step. If the file is accepted, the demonstration contains no logical gap.
That changes the nature of the verification. Nobody needs to read through hundreds of pages: it is enough to run the checker.
We wrote this yesterday and it bears repeating today, because it is the exact point where attention should be focused. A checker guarantees that the demonstration proves what is written in the formalised statement. If that statement does not correspond exactly to the millennium problem — an extra hypothesis, a forcing term, a slightly different framework — the proof is perfectly valid and does not resolve the question posed. It is the most common error in formalisation, and it is precisely what mathematicians will examine first. That review is short: it concerns the statement, not the proof.
The method: 10,000 agents over 88 hours
The figure deserves to be understood rather than admired.
We described this mechanism in relation to the proof obtained in July with sixty-four sub-agents: several instances explore different avenues in parallel, and whatever holds up is kept.
Going from sixty-four to ten thousand is not a change in nature, it is a change of scale. And it says something about the strategy: rather than hoping a model has the right intuition, you launch ten thousand of them and sort mechanically. It is search by intelligent brute force, made possible by an inference cost that has fallen far enough.
This echoes what we noted in our article on the ability of models to have ideas: these systems exploit the known far better than they invent. Multiplying explorations is exactly the way to work around that limitation.
The dispute over priority
The announcement comes with a complication that deserves to be reported precisely.
Tristan Buckmaster, a mathematician at New York University, and Levent Alpöge, a researcher at Anthropic, were working in a neighbouring area. They are the authors of the result on Euler that we covered yesterday.
Buckmaster has publicly raised the question of whether OpenAI accelerated its effort after becoming aware of their work. OpenAI denies that its researchers or its models improperly accessed that work.
We have no way of settling this, and we will not. What we can say is that the situation was foreseeable: when two teams work on neighbouring questions and one of them has considerable computing resources at its disposal, the question of who inspired whom becomes difficult to establish and heavy with consequences.
This is exactly the subject we address this evening in our article on who owns a research question.
The four questions that will decide
Does the formalised statement correspond to the problem? This is the first thing the community will check, and the quickest.
Is the proof file accepted by the checker? Verifiable by anyone with the tool.
Is the result the one that was expected? Demonstrating that a singularity can appear does not answer exactly the same question as demonstrating that it never appears. The official formulation of the millennium problem is precise, and it will be necessary to check which of the variants is being addressed.
Will the prize be awarded? The rules require publication in a peer-reviewed journal and a two-year period of acceptance by the community. In other words: whatever happens, nothing will be official before 2028.
What to take away
We are faced with an extraordinary announcement, with an unusually solid piece of evidence — the formalisation — and a serious challenge to its context.
The right stance is neither enthusiasm nor reflexive scepticism. It is waiting. We wrote last Saturday in our article on what a proof is that a result is only established once someone has been able to challenge it and has failed to do so.
That challenge begins today. It will take weeks, it will be public, and it will probably constitute the most interesting test of the year on the question of what these systems can really do. We will follow the story.