On the early morning of September 8, OpenAI announced a 167-page Navier-Stokes blowup proof with an attached Lean formalization, in a public repository anyone could clone and verify with a single lean command. Two months later, three mathematicians submitted a 25-page preprint arguing that the Lean proof does not match the English original it claims to formalize.
The paper's title says it all: *Navier-Stokes lost in translation*. Lean-verifying an AI's automated formalization does not guarantee the natural-language proof is correct.
The engine passed, but the exhaust pipe is connected to the wrong place
The paper's core accusation comes down to a single character. In OpenAI's English proof, Lemma 8.6's formula (8.19) states an estimate requiring m+4 derivatives on the input side. In the corresponding Lean theorem norm_derivativeWord_inverse_le (repository commit f9e8bc5), two hypotheses require m+5.
One more derivative makes the estimate strictly weaker. The paper notes the constant is defined as K̂_m = max(K_0, K_1, …, K_m); after patching this step by taking a maximum over multi-indices, the resulting estimate is strictly weaker than the original (8.19).
The paper gives a specific cause: the English proof invokes the series Σ 1/(1+|k|)³, for which m+4 derivatives suffice, while the Lean code invokes the series Σ 1/(1+|k₁|+|k₂|)⁴ — the exponent changes from 3 to 4, forcing one extra derivative. Tracing further, this series comes from the Lean theorem coefficient_seminorm_bound.
The authors also audited the whole repository: inverse_finiteJets and mixedJet_inverse_bound carry the same m+5 requirement. Moreover, inverse_finiteJets uses mixed derivatives rather than pure torus derivatives, so it is not even comparable to (8.19).
The paper's wording is restrained: these Lean results are weaker than estimate (8.19) in the English proof.
The chain looks like this:
- English paper, formula 8.19: right-hand side with m+4 derivatives — fed by a series with exponent 3
- Lean theorem: right-hand side with m+5 derivatives — fed by a series with exponent 4
- Result: a strictly weaker estimate, with the constant patched via a max over K₀…Kₘ, a step the paper notes was not done within the original theorem
1. English proof claims a conclusion; AI formalizes it into Lean 2. The Lean compiler accepts → formalization declared successful (this step did pass) 3. But is the generated Lean theorem the one the original intended? Here it is not equivalent — hypotheses were strengthened 4. So Lean is true yet says nothing about the original. And if the original English proof were wrong, the AI would actually be incentivized to find a *different* proof — both outcomes count as success under the compile-based criterion
A seed of divergence visible in the same place
There is another troubling detail. The authors quote the OpenAI repository's own GitHub description: it hosts Lean 4 formalizations of *Finite time blowup for Navier–Stokes* and *Finite time blowup for the Euler equation*. Yet the Lean code uses w = u − v while the original uses w = v − u — a sign difference that propagates into subsequent definitions.
The paper also notes one honest exception: the authors found another similar bound that does appear in the Lean code, but it seems it was not used to prove OpenAI's stated Navier-Stokes theorem — it was proven at compile time but never directly used.
Why this is not a translation-quality problem
The paper elevates the issue to a computability level. The three authors are Alexander Bastounis (King's College London), Fabian Circelli, and Anders C. Hansen (Department of Applied Mathematics and Theoretical Physics, University of Cambridge); Hansen's Solvability Complexity Index (SCI) hierarchy is exactly the tool employed.
The argument has two steps. First, a concrete semantic divergence example: the authors list a recursively enumerable family of polynomials and construct a number r_e = 1/(n_e+1), where n_e is the smallest natural number such that some equation has no natural-number solution. They then write the identity (r_e+1)² = r_e² + 2r_e + 1. To prove this identity in Lean, r_e must first be proven rational — which depends on the decidability of Hilbert's tenth problem. For k ≥ 9 variables, this is impossible.
The paper's positioning is therefore: the ambiguity-resolution problem lies at the infinite height of the SCI hierarchy (SCI = ∞). The halting problem sits at SCI = 1. Informally, semantically faithful automated formalization is harder than any computable problem — one level above the halting problem. The paper states explicitly that no algorithm can perform semantically faithful translation of mathematical prose.
The practical conclusion: this kind of verification guarantees the Lean theorem is true, not that it is the thing you wanted to prove. To answer "is this English argument correct," you must take the second path — a complete semantically faithful translation — which is extremely difficult.
Falling back doesn't help either
The paper also rules out an obvious workaround: back-translate the generated Lean code into English and compare it with the original.
The problem: the back-translation itself must first be proven semantically faithful, and its reasoning must correspond to the original argument. The authors conclude this has the same difficulty as the forward path — just reversed.
The paper also describes the mistranslation mechanism. When the success criterion only checks whether Lean compiles, the AI's behavior is: given a faithful Lean theorem X′ and an English proof Y, rewrite Y′ repeatedly until Lean accepts. This pipeline accepts any valid Lean proof, so if the original English proof were wrong, the AI is incentivized to find a different proof. The authors write explicitly: fixing an error, and replacing a correct argument with a different one, both count as success under this criterion — neither establishes faithfulness to the original argument.
The paper mentions that on October 6 OpenAI released hundreds of mathematical manuscripts. Lean formalization is increasingly treated as a source of trust, but the authors caution that the problem demonstrated in this paper cannot be answered algorithmically. This step of checking still requires human mathematicians' eyes.
The paper only performed a preliminary examination of the Euler proof, saying the "possibility of substantial mistranslations is high" — without a detailed audit or concrete examples.
The paper's disclaimer is explicit: the authors make no claim about the correctness of OpenAI's English proof, only statements about mistranslation. It has not yet passed peer review.
---
Sources: arXiv:2610.08144v1, *Navier–Stokes lost in translation*, submitted 2026-10-06, 25 pages, 4 figures; authors from King's College London and the University of Cambridge; OpenAI repository openai/NavierStokesAndEuler, commit f9e8bc5, files NavierStokes/SmoothFamilyTorusInverse.lean lines 1059–1080 and NavierStokes/R3/PressureFlux.lean line 576, with permalinks provided for verification.