On September 8, OpenAI announced that an internal AI system had produced a proposed solution to the Navier–Stokes existence and smoothness problem. The company released a paper describing its claimed proof, putting an extraordinary proposition before the mathematics community: AI may have helped resolve one of the field’s most difficult open questions.
The announcement deserves attention. It also deserves careful language. A proposed proof, a verified mathematical result, and an accepted solution to a Millennium Prize Problem are different stages of the same story. Meanwhile, a dispute about research credit has raised a second question: how should discovery work when the tools researchers depend on belong to companies pursuing discoveries of their own?
What the problem actually asks
The Navier–Stokes equations describe the motion of fluids, including water and air. They help us study everything from the wake behind a boat to turbulence around an aircraft. The Clay Mathematics Institute’s introduction explains the gap between that practical usefulness and our incomplete mathematical understanding of the equations.
The central issue is whether a smooth three-dimensional flow can remain smooth indefinitely, or whether the equations can develop a singularity in finite time. In the claimed construction, the fluid’s speed grows without bound. “Blowup” is the mathematical term for that behavior.
OpenAI’s paper concerns an initially motionless fluid subjected to a smooth external force. It claims that a singularity develops even while the fluid’s total kinetic energy remains bounded. That combination is possible in the proposed construction because increasingly intense motion concentrates in an increasingly small region. The claim concerns a mathematical model under specified conditions; it does not predict that ordinary water will suddenly accelerate to infinite speed.
The external force matters. Clay’s official problem statement explicitly permits smooth forcing in alternatives C and D. Establishing those alternatives would address an allowed form of the prize problem. It would still leave the corresponding question about unforced Navier–Stokes flow unresolved.
Thousands of agents, one research effort
According to OpenAI’s account, the successful group involved roughly 10,000 concurrent agents using an unreleased model more capable than GPT-6 Astra. The company reports 88 hours to reach the result, followed by 17 hours of Lean formalization and verification using Astra. Researchers redirected resources after progress on Euler’s equations and helped share useful findings between groups.
That is a useful way to understand the scale of the claim. This was an organized research effort involving people, models, tools, and substantial computation. If the proof survives scrutiny, the interesting question will be which parts of that process made the difference: the mathematical ideas, the model’s reasoning, the breadth of the search, or the way intermediate results were checked and combined.
It is too early to assume the same approach will work across other hard problems. But a successful result would give researchers a concrete process to study, beyond another benchmark score.
The dispute over who gets credit
The surrounding mathematical work has its own history. In his discussion of the related results, Terence Tao describes advances by Levent Alpöge and Tristan Buckmaster on fluid equations with smooth forcing, building on work by Diego Córdoba and Luis Martínez-Zoroa. Those earlier ideas and the researchers who developed them belong in any account of this moment.
In his public statement, Buckmaster questions the timing and describes disagreements over release plans and coauthorship, including a proposal he says would have excluded Alpöge. He also describes asking whether their private Codex sessions had been used in training, while making clear that he does not know whether their data was used.
OpenAI’s published response acknowledges that rumors prompted its effort and recognizes the pair’s priority on forced Euler. It denies accessing their unpublished work or specific user data to solve the problem, while acknowledging that it cannot rule out de-identified product-use data helping improve its models. It also says its proofs differ from theirs. The competing accounts leave questions about credit and release discussions unresolved; they do not establish misuse of private research.
The distinction matters. Deliberately consulting someone’s private research and learning from data during model training are different mechanisms. A denial of one does not settle every question about the other. Nor does a shared research direction, by itself, establish that anyone’s private work was used.
For people considering AI as a research partner, the unresolved issue is practical: can they understand where their ideas go, how those ideas may be used, and how their contribution will be recognized? Trust requires answers that are specific enough to assess.
What verification still has to establish
Lean checks the logic of a formal mathematical proof. As the Lean documentation explains, a formal proof establishes that a precisely encoded theorem follows from its definitions and assumptions. That can provide much stronger assurance than simply asking another language model whether an argument looks correct.
The remaining work includes checking that the formal statement matches the mathematical claim, examining the assumptions and dependencies, and independently validating the proof. Formal verification and expert mathematical review can reinforce one another. Neither should be reduced to a badge attached to an announcement.
Prize recognition follows a separate process. Under Clay’s rules, consideration requires publication in a qualifying outlet, at least two years since that publication, and general acceptance by the mathematics community. OpenAI says in its announcement that it does not intend to claim the prize. As of this review, Clay’s problem page still lists Navier–Stokes as unsolved.
Why this matters beyond mathematics
For professionals watching AI’s progress, the implication is worth taking seriously. If systems can help produce original results at this level, we will need to think more carefully about what we delegate and what we remain responsible for understanding.
A convincing answer is only the beginning of useful professional work. We also need to know what supports it, which assumptions it depends on, and whether someone else can check it. When the work involves new ideas, we need a record of the people and prior research that helped make it possible.
That is what makes this announcement consequential even before the final verdict on the mathematics. It brings the promise of AI-assisted discovery into the same room as the obligations of scholarship: explain the result, make it checkable, and give an honest account of how it was reached. The coming scrutiny will test all three.
