Anders Hansen said OpenAI’s OpenAI Navier-Stokes proof error sits in the Lean formalization, where Lemma 8.6 changes a bound from m + 4 to m + 5. The issue matters because OpenAI said the result was also written in natural language, but mathematicians say the two versions do not line up.
Hansen and Lean
OpenAI announced on 8 September that it had found a solution to the Navier-Stokes problem, then published both a natural-language proof and a Lean version. Lean is the formal system that lets a computer check each logical step, so a mismatch in the translation is exactly the kind of error human reviewers have to catch.
Hansen and his team said the mismatch is not a cosmetic difference. The change from below m + 4 to below m + 5 appears in Lemma 8.6, and that is the point they singled out as evidence that the model mistranslated part of the proof when converting it into Lean.
Fabian Circelli on peer review
Fabian Circelli said, “This formalisation process is trying to replace peer review.” That warning fits the practical burden here: if an AI system can shift a bound inside a formal proof, mathematicians still have to read the machine-generated version line by line before trusting the result.
Hansen was careful not to overstate the dispute. “We are not saying that the natural-language proof is wrong,” he said. “Nor do we say that it is correct.” He also said it is entirely possible that both the natural-language proof and the Lean one provide a solution.
OpenAI on Github
OpenAI presents the two proofs as identical on Github, which leaves the dispute focused on whether the Lean formalization really matches the written argument. “This repository contains Lean 4 formalizations of the results presented in [the paper] ‘Finite time blowup for Navier–Stokes’,” Hansen said when describing that presentation.
The unresolved question is whether OpenAI will revise the Lean formalization or defend the version with the changed bound in Lemma 8.6. Until that is settled, mathematicians reviewing AI-written proofs have one clear takeaway: the computer-checkable layer still needs human checking before anyone treats the result as settled.
