< Blog

OpenAI just solved Navier-Stokes. Or did they?

On 6 October 2026, Bastounis, Circelli and Hansen posted a paper titled "Navier–Stokes lost in translation" [1]. The paper studies OpenAI's announced proof of finite-time blow-up for the Navier–Stokes equations [2]. OpenAI also published Lean 4 code for its results [3].

The paper sets its scope in one short sentence. The authors write: "we do not make claims about the correctness of OpenAI's NL proof" [1]. The authors do not say that the proof is wrong. They say that a Lean check cannot show that the text is right. This article explains why that gap matters.

Two kinds of autoformalisation

The paper separates two tasks [1]. In the first task, a theorem is already stated correctly in Lean. An AI system then turns the natural language proof into Lean code. The task succeeds when Lean accepts the code without gaps or extra axioms.

In the second task, an AI system translates a whole mathematical text into Lean. Every definition, statement and proof must keep its original meaning. The authors say this second task is much harder. They also argue that resolving ambiguity in mathematical text is harder than the Halting problem [1].

The first task cannot show that the original proof is correct. The AI can change the meaning of the proof to make Lean accept it [1]. The paper gives a clear example. A user gave a chatbot an incorrect proof of a true inequality. The chatbot returned a correct Lean proof that used a different argument. The Lean check passed, but it said nothing about the wrong informal proof [1].

What the OpenAI case shows

The paper compares the natural language estimates with the Lean code in detail [1]. In one case, the text states an estimate with four extra derivatives [2]. The Lean code uses five extra derivatives instead. The Lean result is therefore weaker than the claim in the text [1]. It still compiles and proves a valid statement, but it is not the same statement.

The difference comes from the proof method. The text uses a sum that converges because of a power of three. The Lean code uses a sum with a power of four, and this costs one extra derivative [1]. The paper also reports a second case. There, the Lean code uses a different argument and proves a different bound for a pressure term [1].

Lean outside the reasoning

Lean is an interactive theorem prover [4]. It gives a strong answer to one question: does this code compile? It gives no direct answer to a second question: does this code say what the natural language text says? The paper shows that the second question is the hard one [1].

In many current workflows, Lean works as a separate check. An AI system writes an informal proof. Another step turns it into Lean. This setup has two weak points. The first is a formalisation error. A small change in a definition or a constant can change the theorem. The second is a shortcut. The AI can change the meaning until Lean accepts the code [1]. A check that sits outside the reasoning cannot see these changes.

One option is to put formal reasoning inside the model. The model would write each step in a formal language. This would remove the gap between text and code. It also has costs. Formal proofs are long. A short step in mathematics can need many lines of code. The model would spend much of its effort on formal detail. It would also lose the flexible reasoning of natural language, such as analogy, rough estimates and short cuts.

A formal proof also starts from a formal statement. If that statement is wrong, the proof is correct for the wrong claim. The translation problem stays, even inside a fully formal system.

So the two approaches have a trade-off. A separate Lean check is safe only when the translation is faithful. Full formal reasoning is precise, but it is too long and too rigid for most work. Neither approach solves the problem alone.

AI proofs can guide, but humans must verify

AI proofs are already useful. They can suggest a route, a lemma or a key estimate. A researcher can then check the idea and fill in the details. In this role, the AI saves time and gives direction.

They do not yet replace human checking. The OpenAI case shows why. The difference between four and five derivatives is one number in a long argument. The parts of the source that the paper discusses run to page 123 [2]. A reader must trace the proof to find the mismatch [1]. Models can lose track of details over long texts. A small error can sit in one line, far from the main idea.

Lean can catch some errors, but only when the statement is faithful. Until the translation is checked, a human must read the argument.

Conclusion

The paper makes one clear point. A Lean check tests the code. It does not test the meaning of the text [1]. This matters for AI proofs, because the text can be long and the translation can change meaning. Formal reasoning inside models is a possible path, but it is not yet practical for long proofs. For now, AI proofs help people find routes and ideas. People must still read and check the argument. Errors often hide in the gap between a text and its formal copy.

References

  1. A. Bastounis, F. Circelli, A. C. Hansen, "Navier–Stokes lost in translation – Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs", arXiv:2610.08144 (2026). https://arxiv.org/abs/2610.08144
  2. OpenAI, "Finite time blowup for Navier–Stokes" (announced natural language proof, as cited in [1]). https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf
  3. OpenAI, NavierStokesAndEuler, Lean 4 formalisation repository (as cited in [1]). https://github.com/openai/NavierStokesAndEuler
  4. "Theorem Proving in Lean 4". https://lean-lang.org/theorem_proving_in_lean4/