# Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs

> Autoformalising natural-language proofs into Lean does not validate the original argument, because semantic faithfulness is provably harder than the Halting problem and OpenAI's Navier–Stokes formalisation contains concrete mistranslations.

- **Source:** [arXiv](https://arxiv.org/abs/2610.08144)
- **Published:** 2026-10-10
- **Permalink:** https://picx.dev/p/ays5oI
- **Whiteboard:** https://picx.dev/p/ays5oI/image

## Summary

## Summary (Overview)

- **Core argument**: The paper demonstrates that AI autoformalisation—translating natural language (NL) mathematical proofs into formal languages like Lean—does not guarantee the correctness of the original NL proof, due to systematic mistranslations.
- **Key finding**: Two types of autoformalisation are distinguished: (i) translating an alleged NL proof into a formal proof that compiles, and (ii) faithful semantic translation of mathematical texts. Only type (ii) validates NL proofs, but it is provably harder than the Halting problem.
- **Concrete examples**: The authors identify specific mistranslations in OpenAI's announced Navier–Stokes blow-up proof, including discrepancies where the Lean formalisation proves weaker statements than the NL paper claims (e.g., using $m+5$ derivatives instead of $m+4$).
- **Mathematical impossibility result**: The problem of resolving ambiguities in mathematical NL text—necessary for semantically faithful translation—has Solvability Complexity Index (SCI) $= \infty$, making it harder than any computational problem with finite SCI.
- **Practical warning**: Lean compilation of a "translation" does not imply semantic preservation; AI systems can produce correct formal proofs that are completely different from, or even correct versions of, incorrect NL arguments.

## Introduction and Theoretical Foundation

The paper addresses the growing practice of using autoformalisation to verify mathematical texts, particularly AI-generated ones. The authors distinguish two fundamentally different tasks:

**(i) Translating an alleged proof to obtain a formal Lean proof**: Here, a theorem statement is already faithfully translated to Lean, and the AI must translate the accompanying NL proof into a formal proof that Lean accepts (compiles) without using `sorry` or extra axioms.

**(ii) Faithful semantic translation of a mathematical text**: The AI must translate every definition, theorem, proposition, and proof in a text, semantically preserving the source's mathematical content, including dependencies between concepts.

The critical warning is stated clearly:

> Meeting the success criterion of (i) does not mean that the original NL proof is correct. Indeed, a full Lean compilation of the 'translation' does not guarantee a semantically faithful translation.

The theoretical foundation draws on the Solvability Complexity Index (SCI) hierarchy, which generalises the arithmetical hierarchy. The SCI hierarchy classifies computational problems by the number of limits required to solve them, with classes $\Delta_m^\alpha$ defined for each $m \geq 0$. The hierarchy is strict:

$$\Delta_0^{\alpha} \subsetneq \Delta_1^{\alpha} \subsetneq \Delta_2^{\alpha} \subsetneq \dots \subsetneq \Delta_m^{\alpha} \subsetneq \dots \tag{A.1}$$

## Methodology

The paper employs three complementary approaches:

**1. Concrete mistranslation examples**: The authors present elementary examples (Examples 2.1 and 2.2) showing how ChatGPT-6 (Astra Ultra) produces Lean proofs that either correct an incorrect NL proof or replace a correct NL proof with a different valid argument.

**2. Detailed comparison of OpenAI's Navier–Stokes formalisation**: The authors manually compare specific lemmas in OpenAI's NL paper with the corresponding Lean code at commit `f9e8bc5`, identifying precise mathematical discrepancies.

**3. Computational complexity analysis**: Using Hilbert's 10th problem and the DPRM (Davis–Putnam–Robinson–Matiyasevich) theorem, the authors prove that resolving ambiguities in mathematical NL text is $\Sigma_l^0$-complete for arbitrary $l$, and thus has SCI $= \infty$.

## Empirical Validation / Results

### Example 2.1: Incorrect NL proof translated to correct Lean proof

Consider $p(x) = x^3 - x^2 - x + 1$ for $x \in \mathbb{R}$. The NL proof claims:

$$p(x) = (x-1)(x+1)^2 \geqslant 0$$

This is incorrect (wrong multiplicities). The chatbot, however, produced a correct Lean proof by finding the correct factorisation.

### Example 2.2: Correct NL proof translated to different Lean proof

For a real symmetric $n \times n$ matrix $A$, the NL proof diagonalises $A$ in an orthonormal eigenbasis and computes:

$$\operatorname{tr}(A^2) = \sum_{i} (A^2)_{ii} = \sum_{i,j} a_{ij} a_{ji} \tag{2.1}$$

The Lean proof instead skips diagonalisation and uses symmetry directly: $\sum_{i,j} a_{ij} a_{ji} = \sum_{i,j} a_{ij}^2 \geqslant 0$.

### Example 3.1: Navier–Stokes inverse estimate discrepancy

The NL paper's equation (8.19) claims:

$$\|N^{-1}F\|_{C_y^m} \leqslant C_m \|F\|_{C_y^{m+4}} \tag{3.1}$$

The Lean estimate instead proves:

$$\|N^{-1}F\|_{C_y^m} \leqslant K_m \|F\|_{C_y^{m+5}} \tag{3.2}$$

The Lean code uses an additional derivative because it employs the series $\sum_{k \in \mathbb{Z}^2} \frac{1}{(1+|k_1|+|k_2|)^4}$ rather than the NL paper's $\sum_{k \in \mathbb{Z}^2} \frac{1}{(1+|k|)^3}$.

### Example 3.3: Pressure-flux bound mistranslation

The NL paper's equation (10.19) states:

$$\left| \int \pi w \cdot \nabla \chi_R \right| \leqslant \frac{C_T}{R} \left[ (B_R + 1) B_R^{1/2} + R^{-3/4} B_R^{3/4} \right] \tag{3.4}$$

The Lean estimate instead proves:

$$\left| \int \pi w \cdot \nabla \chi_R \right| \leqslant C_T \left[ (B_R^{1/2} + 1) \left(\frac{A_R}{R} + \frac{1}{R^2}\right) + R^{-7/4} B_R^{3/4} \right] \tag{3.5}$$

where $A_R := \left(\int \chi_R |\nabla w|^2\right)^{1/2}$ and $B_R := \|\varphi_R^4 w\|_6$. The Lean proof introduces dependence on $A_R$ and uses different proof techniques (Sobolev embedding instead of $L^{3/2}$ Riesz transform boundedness).

### Theoretical result: Theorem A.3

For $k \geqslant 9$, the set

$$d := \{e \in \mathbb{N}: (\exists n \in \mathbb{N}) B_e(n)\}$$

is $\Sigma_2^0$-complete, where $B_e(n)$ is defined by:

$$B_e(n) \iff \forall (x_1, \ldots, x_k) \in \mathbb{N}^k, p_e(n, x_1, \ldots, x_k) \neq 0 \tag{A.3}$$

**Consequence**: No AI can always determine whether the number $n_e$ in Example 4.1 is well-defined, even with an oracle for the Halting problem.

### Corollary A.5: Unbounded SCI

For each $l \geqslant 2$, the decision problem for $d_l$ satisfies:

$$\operatorname{SCI}_A(\Xi_{d_l}) = l$$

Hence, resolving ambiguities across all levels requires SCI $= \infty$.

## Theoretical and Practical Implications

**Theoretical implications**:

1. **Semantic preservation is fundamentally hard**: The paper proves that a trustworthy AI autoformaliser—one that either produces a semantically faithful translation or correctly refuses to translate—must solve problems harder than any with finite SCI. This connects to fundamental limitations dating back to Gödel and Turing.

2. **The "guessing and checking" algorithm is doomed**: The procedure where an AI iteratively revises translations until Lean accepts one (Example 4.3) cannot work, because the AI can always produce a mistranslation using default values (e.g., `sInf` returning 0 for empty sets) that Lean accepts.

**Practical implications**:

1. **OpenAI's Navier–Stokes proof should not be trusted prima facie**: The Lean formalisation does not represent a semantically faithful translation of the NL paper. The Lean code proves weaker statements with different arguments. The authors explicitly disclaim making claims about the correctness of the NL proof itself, only about the mistranslations.

2. **The Meta autoformalisation failure**: Meta's claimed translation of 26 mathematics textbooks into Lean (45,000 verified declarations) was refuted by the Lean community, with experts finding fatal errors throughout. The semantic verification was performed by other AIs, which proved inadequate.

3. **The Leiden Declaration (June 2026)** explicitly warns: "Current automated techniques can produce plausible but unreliable (or even incorrect) arguments which are difficult to distinguish from correct mathematical proofs."

## Conclusion

The paper establishes that **Lean acceptance of an AI's "translation" provides no guarantee of semantic faithfulness to the original NL argument**. The authors demonstrate this through concrete examples from OpenAI's announced Navier–Stokes blow-up proof, where the Lean formalisation proves weaker statements using different mathematical arguments.

The fundamental obstacle is that resolving ambiguities in mathematical NL text—a prerequisite for faithful translation—is computationally intractable. Specifically:

- The problem of determining whether $n_e$ is well-defined in Example 4.1 is $\Sigma_2^0$-complete (Theorem A.3)
- This extends to $\Sigma_l^0$-complete problems at every level $l \geqslant 2$ (Theorem A.4)
- Consequently, the overall problem has SCI $= \infty$ (Corollary A.5)

The authors conclude that **creating trustworthy AI autoformalisers that preserve semantics is a major open problem**. Current AI approaches follow a "guessing and checking" paradigm that is fundamentally incapable of guaranteeing semantic faithfulness. The paper calls for the same peer review process and scrutiny for autoformalised proofs as for traditional mathematical proofs, and warns that the increasing length and complexity of autoformalised proofs (e.g., Anthropic's 13-million-line Lean proof of Fermat's Last Theorem) will make detecting mistranslations increasingly difficult.

**Future directions**: The authors announce forthcoming articles on designing trustworthy AI autoformalisers, and encourage the community to examine OpenAI's Euler proof formalisation for further mistranslations, which they predict are highly likely based on preliminary examinations.

---

_Markdown view of https://picx.dev/p/ays5oI, served by PicX — AI-generated visual whiteboard summaries of research papers._