OpenAI and Navier–Stokes: what has been proven, what has not, and why there is controversy

On September 8, 2026, OpenAI announced that an internal model had produced a proof about the Navier–Stokes equations, one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Headlines around the world reported it as the moment a machine solved a problem that had been open since 2000.

The real story is more nuanced. There is a serious mathematical result, a technical caveat that significantly changes its scope, two Spanish mathematicians at the origin of the idea, an authorship dispute with mutual accusations, and a deeper objection about what AI is doing to research.

What exactly has OpenAI announced?

An internal model, described by the company as significantly more capable than GPT-6 Astra and whose training began on August 28, worked on the problem with around 10,000 agents in parallel. The run consumed close to 2.7 million messages and about 130 billion output tokens over roughly 88 hours. Sébastien Bubeck of OpenAI put the compute cost at several million dollars.

The result is a proof that the dynamics of the Navier–Stokes equations can develop a finite-time singularity. In plain terms, a fluid described by those equations can reach a point where the mathematical solution stops making sense, with quantities blowing up to infinity.

After the proof, another model—this time GPT-6 Astra—spent 17 more hours formalizing the argument in Lean, a proof assistant that mechanically checks every logical step. The certificates are published in an open repository.

This is how the fluid behaves near the singularity. Orange marks the regions that rotate faster and turquoise the slower ones, and the trajectories spiral inward as the fluid stretches along the axis. Source: OpenAI.

What are the Navier–Stokes equations and why do they matter?

They are the equations that describe the motion of fluids, from air around a wing to water through a pipe or blood through an artery. They are used daily in aeronautical engineering, climatology, engine design, and industrial simulation, and they work well in practice.

What no one had proved is that they are always well defined. The Millennium Prize problem asks whether, starting from a smooth, well-behaved three-dimensional fluid, the equations guarantee a smooth solution forever, or whether they can break down at some point. It is a question about the foundations, not about usage.

But note: even if the result is fully confirmed, it will not change any engineering calculation tomorrow. Real fluids have molecular structure, and the equations stop applying long before reaching a mathematical singularity.

Does OpenAI get the million dollars?

No—the company itself says so. In its publication, it states that it is not claiming the Millennium Prize for this result.

The reason is a technical nuance that most headlines skipped. The official statement drafted by Charles Fefferman for the Clay Institute includes several formulations. The ones that qualify for the prize refer to the fluid without external force, left to evolve on its own. What OpenAI has proved corresponds to the formulations with forcing, that is, with a smooth force applied from outside that pushes the fluid toward the singularity.

The difference is not cosmetic. Constructing a tailored force that drives the system to blow up is a very hard problem, though still considerably less hard than proving the fluid can break down on its own. Strictly speaking, the Millennium Prize problem remains open.

On top of that is the procedure. The Clay Institute’s rules require publication in a top-tier journal and two years of community scrutiny before awarding anything. As of today, there is no official validation from the institute.

Who actually contributed the ideas?

This is the part that has been little reported in Spain. The analytical strategy underpinning the result comes from the work of Diego Córdoba, from Madrid’s Institute of Mathematical Sciences and a National Research Award winner, and Luis Martínez-Zoroa. They had spent years building the method that makes it possible to construct singularities in this type of equation.

Charles Fefferman, who drafted the official statement of the problem, summed it up bluntly by saying that the heroes of this story are Córdoba and Martínez-Zoroa. Tristan Buckmaster of New York University has even suggested that Martínez-Zoroa’s work deserves a Fields Medal.

In other words, the AI did not start from scratch. It moved very quickly along a path that two human mathematicians had opened and signposted.

Why is there an authorship dispute?

Buckmaster and Levent Alpöge, a researcher affiliated with Anthropic, were working in parallel on the forced Euler equations, with an approach that extended that of Córdoba and Martínez-Zoroa. They published their results on September 7, one day before OpenAI’s announcement.

Buckmaster says OpenAI contacted him on September 6 to tell him they had a hundred-page proof obtained with the same approach, and that when he asked when they had issued those instructions to the model, the answer was in the last few days, right after learning of his work. He adds that they offered him co-authorship while asking to leave Alpöge out because he works at a competing company, and he describes pressure when he tried to make it public.

OpenAI rejects the accusations, calls them false, congratulates both researchers on their work, and says it recognizes their priority. Bubeck publicly apologized for what he called a very unfortunate choice of words about authorship. The company did admit one point that deserves attention: de-identified data from the use of its products may have contributed to improving its models.

Buckmaster, for his part, acknowledges that he has not seen OpenAI’s proof and does not know what the model did or how. With the public information available, neither version can be considered settled.

Is it not enough that Lean verified it?

Lean contributes a great deal, but not everything—and this distinction is the most useful takeaway from the entire episode. What Lean certifies is that the theorem follows logically from the written hypotheses, step by step, with no gaps. That immediately eliminates the kind of error that has brought down famous proofs throughout history.

What Lean cannot judge is whether the written hypotheses are the right ones. If, during formalization, a different decay condition slipped in, a more convenient function space, or a definition of smoothness for the forcing that is not the one in the official statement, the code still compiles and the theorem proved is a different one. Human review is still necessary, only now it focuses on the statement rather than the proof.

The deeper objection, according to Terence Tao

Terence Tao, probably the most influential living mathematician in this area, has raised a critique that goes beyond who signs what. His argument is that the value of an open problem is not only in the answer. It is in the tools and ideas generated while trying to solve it, which almost always end up being worth more than the specific result. When an autonomous AI produces the solution in private, without showing the process or the dead ends, the field is left with the result and without the learning.

Tao framed it with a stark image: indiscriminate exploitation of open problems that can destroy the ecosystem from which the next generation of techniques, problems, and mathematicians would have emerged. He also warns of a side effect: a quick answer discourages those who were exploring other paths. It is an objection about the method, not the capability. No one disputes that the system did something remarkable.

What would this discovery mean?

It is worth separating what changes tomorrow from what changes over ten years:

In engineering, little in the short term. No aerodynamics or climatology calculation will be redone because of this. Real fluids have molecular structure, and the equations stop describing them long before reaching a mathematical singularity. What changes is the model’s status: knowing it can break down forces greater precision about the conditions under which a simulation is reliable, and that precision does eventually make its way into the software used every day.

In mathematics, a shift in the profession. If the pattern repeats, the researcher’s work shifts from finding the proof to formulating the problem correctly and verifying what the machine returns. Formalization in assistants like Lean stops being a niche specialty and becomes infrastructure, because it is the only way to audit at scale what an automated system produces.

In artificial intelligence, the bar moves. Until now, the benchmark was solving problems with known solutions. This episode, if it holds up, points to something else: generating new, verifiable knowledge. It also brings with it an expensive method—massive compute as a way of doing research, with thousands of parallel attempts and an objective filter that keeps the ones that survive.

In companies, it brings the timeline forward. What today requires ten thousand agents and several million dollars for an open problem will, in a couple of years, resemble what you can run on a well-scoped internal problem. It also changes what is considered an acceptable deliverable, because the result starts to come with its verification instead of requiring an act of faith.

If you are considering how to apply agents with verification and control in your organization, at LISDATA we develop that design through our AI agent consulting for businesses.