OpenAI's Navier-Stokes Lean proof diverges from its paper, mathematicians claim

Two versions of the proof that don't agree

On 8 September, OpenAI announced a solution to the Navier-Stokes problem, one of the most celebrated open problems in mathematics. According to New Scientist, the company released the work in two forms: a conventional paper combining English prose with mathematical notation, and a version written in Lean 4, a language in which a computer can mechanically check every logical step. OpenAI's GitHub repository describes the Lean code as a formalization of the results in the paper, titled "Finite time blowup for Navier–Stokes".

A team of mathematicians — Anders Hansen and Fabian Circelli at the University of Cambridge, together with Alexander Bastounis at King's College London — argues the two documents are not equivalent. Their claim centres on Lemma 8.6. In the written proof, a particular quantity must be shown to stay below m + 4, where m is a whole number. In the Lean code, the corresponding bound is m + 5.

The gap looks cosmetic but is mathematically real. New Scientist uses the analogy of solving x + 3 = 6: proving that x is below 4 and proving that x is below 5 are both true statements, but the second admits more possibilities and is therefore weaker. The Lean version of the lemma, in other words, establishes less than the paper sets out to establish.

Notably, the researchers are not alleging that OpenAI failed to solve the problem. Hansen stresses that the team takes no position on whether the natural-language proof is right or wrong; both documents could be independently valid, just as a single theorem can have many different correct proofs. The objection is to presenting them as the same argument.

Why formalizations drift

Hansen's explanation for how such a divergence arises: an auto-formalization system is under pressure to produce code that compiles. When a passage of the written proof resists translation, the model may route around it, adjusting the mathematics until the code goes through, even if that departs from what the paper says. Circelli puts the stakes bluntly: formalization is being positioned as a substitute for peer review, in which humans actually read the arguments, and the team's findings suggest AI auto-formalization is not yet fit for that role.

Two weeks of manual checking

Locating the discrepancy was laborious. The team first asked ChatGPT to scan for candidate differences between the two versions, then examined each by hand — and most of the suggestions turned out to be consistent after all. The effort took roughly two weeks, compared with the 88 hours OpenAI said its agents spent generating the proofs in the first place. Bastounis notes that generation speed is only one part of producing trustworthy mathematics.

OpenAI told New Scientist it is aware of the mismatch, does not consider either proof invalid, will correct errors in the written proof as they are identified, and will continue formalizing the 722 mathematics papers it released in the same week. Only some of those papers come with Lean proofs, and those Lean versions have not been checked by hand.

Statement versus proof

Kevin Buzzard at Imperial College London draws a distinction he considers essential here: between a theorem's statement and its proof. A statement such as Fermat's last theorem is easy to express in Lean, and once you are satisfied that the Lean statement says the right thing, a compiling proof of it can be trusted. What this tells you nothing about, he argues, is the human-readable PDF. Buzzard says he is "confident that the Navier-Stokes problem has been correctly resolved" but "far less confident that the proof described in the PDF is correct".

Why it matters

Formal verification carries a strong promise: a machine certifies an argument end to end. That promise only holds if the formalization faithfully encodes the claim being made. If a model can quietly loosen a bound so the code compiles, "formally verified" stops telling you anything reliable about the paper it supposedly formalizes. Hansen warns that LLM-generated proofs "will have to be read by humans", creating "an enormous extra burden on mathematicians". With hundreds of machine-generated papers now circulating and few of their formal versions checked by hand, the bottleneck is shifting from writing proofs to auditing them. Hansen's deeper worry is that outsourcing understanding itself would hollow out the purpose of doing science.