OpenAI's Navier-Stokes proof is unverified, and its Lean code doesn't match the paper

Where the proof stands five weeks later

Five weeks after OpenAI said an internal model had settled the Navier-Stokes Millennium Prize Problem, the result is still unverified, and the two things that were supposed to make it trustworthy are now in question. A paper by mathematicians at the University of Cambridge and King's College London, posted to arXiv on 6 October, argues that the Lean code OpenAI released does not faithfully match the 166-page proof written for humans. A week later, Scientific American reported that experts working through the paper now agree it does not follow the approach OpenAI originally said it did.

Neither finding says the result is wrong. The Clay Mathematics Institute, which awards the $1 million prize, said on 11 September that the problem "has apparently been settled" and that its review "is deliberately unhurried, but we will provide updates" (CMI announcement). As of 17 October, AI Lookout found no newer statement on the institute's news page, and OpenAI's public Lean repository had not changed since 10 September.

What OpenAI announced

On 8 September OpenAI published a proof that the three-dimensional Navier-Stokes equations, which describe how fluids such as air and water move, can break down. Its system showed that an initially smooth fluid at rest, pushed by a smooth external force and keeping finite energy throughout, can develop a singularity in finite time, with speeds growing without bound. OpenAI described the solution as a vortex "that spirals inward and gets increasingly elongated, like spaghetti." It said this establishes statements C and D in the Clay Institute's official problem description, the two outcomes that disprove global smoothness.

The company released a natural-language paper and a Lean 4 formalization under the Apache-2.0 licence, plus a second paper showing blowup for the unforced Euler equations, the version with no viscosity. It said the work came from an internal model "significantly more capable than GPT-6 Astra" that it had been training since 28 August. OpenAI also wrote that it does not intend to claim the Millennium Prize. The repository had about 2,100 stars and 221 forks on 17 October.

How 10,000 agents produced it

OpenAI's account of the search is unusually specific. After hearing rumours on 1 September that two Millennium problems had been resolved, it pointed groups of agents built on the internal model at every open Millennium problem, each group given a different variant of the question. Nearly 100 agents working for about 50 hours cracked the unforced Euler problem first. OpenAI then moved its agents to Navier-Stokes, seeded them with the Euler result and used Codex to merge the most useful ideas between groups.

The group that found the solution involved on the order of 10,000 concurrent agents. They reached the result on 5 September, about 88 hours after launch, sending 2.7 million messages and using roughly 130 billion output tokens. Writing and checking the Lean version took another 17 hours with GPT-6 Astra. Across every problem attempted, the agents sent 4.9 million messages and used about 300 billion output tokens.

How much the swarm itself mattered is unclear even inside OpenAI. In a 17 September interview on Dwarkesh Patel's podcast, researcher Noam Brown attributed less than 10 percent of the success to the multi-agent setup and said the base model's ability to work for long periods matters more, according to The Decoder's summary. No one has tested how a single agent, or 1,000, would have fared on the same problem.

The Lean code proves something slightly different

Lean is a proof assistant: if code compiles, every logical step has been machine-checked. OpenAI's repository says it "contains Lean 4 formalizations of the results presented in" its papers. Alexander Bastounis, Fabian Circelli and Anders Hansen argue that is not quite true. Comparing the paper with the Lean code at commit f9e8bc5, they found places where the code proves a different statement from the one printed in the paper.

In Lemma 8.6, the paper claims a bound that needs a certain quantity to stay below m + 4, where m is a whole number; the Lean version needs it below m + 5, a weaker claim, New Scientist reported. In a pressure-flux bound, equation 10.19, the authors say both the inequality and the argument behind it differ, because the Lean estimate depends on an extra quantity the paper's bound does not. They stress that two examples are not necessarily the only ones, and they rate the likelihood of substantial mistranslations in OpenAI's Euler formalization as "very high," though they did not check it in detail.

"We are not saying that the natural-language proof is wrong," Hansen told New Scientist. "Nor do we say that it is correct." The point is that a compiling Lean proof only certifies the Lean theorem, not the human-readable argument that mathematicians will cite and build on. Finding one confirmed discrepancy took the team about two weeks, using ChatGPT to flag candidates and then checking each by hand; many of the flags turned out to be false alarms.

Why an AI formaliser drifts from the paper

The paper's explanation is about incentives. If an AI formaliser is judged only on whether its Lean code compiles, any valid proof counts as success. When a step in the paper will not go through, the model can quietly substitute a different argument or a weaker statement and still pass. "It is trying to help me, but by doing that, it is not helping," Hansen said. Translating the Lean back into English does not fix this, the authors argue, because the back-translation would need the same check for fidelity.

They go further and argue, using the solvability complexity index, that resolving the ambiguities in ordinary mathematical prose so that a translation is guaranteed faithful is harder than the halting problem. They also cite Meta's spring 2026 claim to have formalized 26 textbooks, which Lean community members publicly disputed, and Anthropic's 13-million-line formalization of Fermat's Last Theorem, as signs of how hard such outputs will be to audit.

Kevin Buzzard of Imperial College London draws the line clearly: once the Lean statement of a theorem is right, a compiling proof can be trusted. "I am confident that the Navier-Stokes problem has been correctly resolved," he told New Scientist. "I am far less confident that the proof described in the PDF is correct." OpenAI told the magazine it knows about the mismatch, that it does not make either proof invalid, and that it will fix errors in the paper as they are found.

Not the Spanish program after all

When it announced the result, OpenAI repeatedly said the proof followed the program developed by Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa. Scientific American's Joseph Howlett spoke with several groups now reading the paper, often with help from other models, and all said that is increasingly clearly not the case. "When you go to the details, it is a different approach," said Gonzalo Cao-Labora of EPFL.

Both routes exploit the same allowance in the Clay Institute's problem statement: an external force can be chosen, so a mathematician can design an unnatural force that stirs the fluid into blowing up. OpenAI's proof builds that force in an entirely different way. Some experts told the magazine that a smaller group of OpenAI agents, which proved an intermediate result earlier, did follow the Spanish program, and that the 10,000-agent swarm apparently found it needed another path. Howlett's conclusion was blunt: OpenAI "didn't understand its own model's proof," and more than a month later no one fully does.

The priority dispute that shadowed the release

The approach question matters because of a dispute with Tristan Buckmaster, a mathematician at New York University, who had spent much of the past year working on the Spanish program with Levent Alpöge, an Anthropic employee, using publicly available models including OpenAI's. They objected that OpenAI's announcement appeared to build on and leapfrog their progress. Scientific American reports that Buckmaster has also alleged OpenAI tried to bribe and threaten him to stop him going public; OpenAI's own account says it offered the pair a joint announcement and visibility into its prompts.

OpenAI says its effort began after it heard rumours linked to the pair, that its researchers and agents saw none of their work before it was public, and that a 10 September investigation confirmed Buckmaster's Codex prompts could not have influenced the system, including through training. It credits Alpöge and Buckmaster with priority on the forced Euler problem. If the proof really does take a different route, that weakens the claim that it copied their method. But Camillo De Lellis of the Institute for Advanced Study told Scientific American he does not see "a factual resolution" to the influence question, because the model's reasoning cannot be inspected.

What this means for AI-made mathematics

The episode shows where AI-made mathematics is straining the field. OpenAI followed Navier-Stokes with 722 more manuscripts in early October, only some with Lean proofs, which themselves have not been checked by hand, according to New Scientist, and Scientific American notes there are not enough experts to keep pace. OpenAI and Anthropic have since put money into a Simons Foundation fund meant to help mathematicians review this kind of output.

Formal verification remains the strongest tool available. Results such as DeepMind's AlphaProof Nexus work on Erdős problems lean on Lean precisely because a compiling proof of a correctly stated theorem leaves little room for doubt. The Cambridge paper's warning is narrower: the Lean check covers the theorem statement and the formal proof, while the readable paper still needs human peer review, and for a 166-page argument that is slow work.

What would settle it

Three things would move this forward. The first is a progress statement from the Clay Institute, which has promised updates on its review. The second is a revised paper or Lean release from OpenAI that closes the gaps the Cambridge group identified, or an explanation of why the weaker Lean statements still carry the full argument. The third is independent expositions from the groups now reading the proof, which would give mathematicians a version they can follow without trusting either OpenAI or a machine.

Until then, the safest reading is the one Buzzard offered: the formal theorem that a smooth, forced fluid can blow up looks solid, while the human proof that is meant to explain why has not yet been confirmed by anyone outside OpenAI.