OpenAI's Navier–Stokes claim comes with a Lean proof. Its provenance is contested.

OpenAI published a post on Tuesday titled “On the Navier–Stokes Millennium Prize Problem”, saying it was sharing an AI-generated solution to one of the seven Millennium Prize problems, together with a writeup and a formal proof in Lean. Earlier the same day, NYU mathematics professor Tristan Buckmaster announced three proofs of his own, with Anthropic mathematician Levent Alpöge — and alleged that OpenAI had learned of their unpublished approach, pushed it through to the harder equation first, and then pressed him over authorship.

What was actually proved

The Navier–Stokes equations describe how fluids move, and the Millennium Prize problem asks something that sounds simple: starting from smooth conditions, do the solutions stay smooth forever, or can they break down in finite time? OpenAI's answer is that they can break down.

The Lean formalization published alongside the writeup, in the repository openai/NavierStokesAndEuler, states the result precisely. For any positive viscosity, it proves that smooth initial data and a smooth forcing term exist on ℝ³ for which no global smooth solution keeps its kinetic energy uniformly bounded, and separately that the same holds for smooth periodic data on the torus ℝ³/ℤ³. The repository says these correspond to alternatives (C) and (D) in the Clay Mathematics Institute's official description of the problem.

The forcing term is the part to hold on to. Alternatives (C) and (D) are the breakdown branches of the official statement, and they permit an external force to be applied to the fluid. Buckmaster, who had chosen the same route, described it this way in the statement announcing his own proofs:

The route to the Clay problem through a smooth force, options c and d in Fefferman's statement of the problem, is the route Luis and Diego opened and the one Levent and I had quietly chosen to attack.

The same repository also carries a separate Euler result with no forcing at all: a smooth, compactly supported, divergence-free initial velocity on ℝ³ that develops a singularity in finite time, with the C¹ norm becoming unbounded and the vorticity integral diverging. That distinction — forced versus unforced — matters for the dispute as well as for the mathematics.

A machine-checkable proof is not the same as a settled one

The formalization targets Lean 4.34.0-rc2 with Mathlib, and the repository ships a ComparatorChallenges directory with instructions for independently checking the proof. That is more than most claimed breakthroughs offer on day one: anyone with the toolchain can run the check rather than take the claim on trust.

It is worth being precise about what such a check buys. Lean verifies that the proof follows from the statement as formalized. It does not verify that the formalized statement is the one the mathematical community means by the Millennium Prize problem, and it does not verify the accompanying prose. Reading the formal statements against Charles Fefferman's official wording — including whether the forcing term meets the bounds the statement requires — is human work, and it has not happened yet. The post went up today; no peer review has taken place.

The credit dispute

According to TechCrunch, which published Buckmaster's account on Tuesday, he and Alpöge were finalizing their own results when they learned that “information about our progress had been passed to OpenAI”. When they made contact, they were told OpenAI already had a full proof of the central problem. Follow-up questions about when OpenAI had begun and how much human input was involved, Buckmaster said, drew evasive answers.

His suspicion rests on how unusual the approach is. “Almost nobody else I know of was working on it,” he said of the smooth-force route. “It is not the direction one arrives at in a few days by giving a model the problem statement.”

Buckmaster further alleges that Sébastien Bubeck, who leads OpenAI's math team, proposed dropping Alpöge — an Anthropic employee, though not working on Anthropic's behalf — from the credit as part of a compromise, and that when Buckmaster said he would make the dispute public, Bubeck replied “Why would you ruin your career?” and later “If you don't want me to be nice, then I don't have to be nice.” These are Buckmaster's characterizations of private conversations. We were not able to open a source carrying Bubeck's own response to them, and they should be read as one party's account.

OpenAI's post addresses the provenance question directly, in a passage TechCrunch quotes:

We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs unforced).

The post also confirms that OpenAI's effort began on 1 September, prompted by rumours that two Millennium Prize problems had been solved, and that conversations with Buckmaster and Alpöge took place. TechCrunch reports the week-long push consumed 300 billion output tokens across several problems, which it estimates at roughly $22.5 million if charged at current Astra API rates. The Clay Mathematics Institute attaches a $1 million prize to each of the seven problems.

What it changes for people building with these tools

Two of the lessons here are practical rather than mathematical.

• Formal verification is becoming the credible way to ship an AI-produced result. A Lean file anyone can run is a stronger claim than a benchmark number, and it is the artifact to ask for when a model's output has to be trusted rather than skimmed.
• Coding-agent transcripts are a data-governance question, not only a privacy one. TechCrunch notes that OpenAI reserves the right to train on Codex interactions, with an opt-out available, and that Buckmaster used Codex extensively on unpublished work. Whatever happened in this case, the general lesson stands: if you are working on something novel or confidential inside a lab's coding agent, check the retention and training settings before you start, not after.
• Scale has become a strategy, not just a cost line. A week of parallel agents at a reported 300 billion output tokens is a method available to very few organizations, and it changes who can move first once an approach is known.

None of this settles the mathematics. The proof is public and machine-checkable, which means the next few weeks of specialist reading will decide whether the formal statements match the problem Clay actually posed, and whether a forced construction is accepted as a resolution or as a strong result adjacent to one. The credit question will be settled, if at all, by people rather than by Lean.

A note on sourcing: OpenAI's post page blocks automated clients, so we did not read it directly. We verified the announcement, its title and its timestamp through OpenAI's own news feed, read the published Lean repository, and relied on TechCrunch's direct quotations from the post itself.