Glonce

Paper says Lean version of OpenAI's Navier-Stokes proof does not match the original

researchThe Glonce editorsHacker News🔥72Glonce rating72Impact55Novelty60Relevance85Surprise60Players45Credibility80

A paper submitted to arXiv on 6 October 2026 (Mathematics, Analysis of PDEs) takes aim at a growing practice: using AI to translate a mathematical text from natural language (NL) into a formal language such as Lean, then verifying the formal version by machine. The abstract notes that this approach is increasingly used to verify mathematical texts, including AI-generated ones, and gives OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations as an example of such a text.

The authors' central point is that this process may offer no confidence in the original NL argument. Once the AI has translated the text, the formal argument can easily be checked mechanically, but that check only speaks for the translation. Whether the translation is semantically faithful is a separate question, and the authors say it is hard to get right.

They make the difficulty precise with a complexity claim. Resolving ambiguities in mathematical NL text, which a semantically faithful translation requires, is, in their words, arbitrarily high in the Solvability Complexity Index (SCI) hierarchy and the arithmetical hierarchy; they write SCI = infinity. For comparison, the Halting problem has SCI = 1. From this they conclude, stating it informally, that providing semantically faithful AI autoformalisation is harder than any computational problem, including the Halting problem.

To show the effect in practice, the paper gives several examples of AI mistranslations of NL statements and proofs into Lean, each producing a mismatch between the NL proof and its Lean 'verification'. OpenAI's announced Navier-Stokes proof is among them. The authors report that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.

The submission history lists Alexander Bastounis as the sender of version 1, posted on 6 October 2026 at 10:58 UTC (1,080 KB).

Key facts

  • The paper (arXiv, math.AP, submitted 6 Oct 2026) argues that machine-checking an AI-produced Lean translation may give no confidence in the original natural-language argument.
  • The authors say resolving ambiguities in mathematical natural-language text is arbitrarily high in the SCI hierarchy (SCI = infinity), versus SCI = 1 for the Halting problem.
  • Stated informally, faithful AI autoformalisation is harder than any computational problem, including the Halting problem.
  • The paper gives several examples of AI mistranslations into Lean, including OpenAI's announced Navier-Stokes proof.
  • For that proof, the authors show the formalised Lean proof does not correspond to the natural-language proof of blow-up of solutions to the Navier-Stokes equations.

Why it matters

Formal verification is often presented as the way to trust AI-generated mathematics: translate the proof into Lean, let a machine check it. This paper says the weak link is the translation step. If an AI system renders the text unfaithfully, a successful Lean check certifies the wrong statement. The paper applies the point to a high-profile case, OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations, where the authors say the Lean proof does not correspond to the natural-language proof.

Who it affects

Mathematicians and AI labs that use autoformalisation to verify mathematical texts, including AI-generated ones, and anyone weighing a claim that rests on a Lean verification. It bears directly on OpenAI's announced Navier-Stokes proof, which the paper examines.

How to use it

This is a research paper, not a product or tool. The practical lesson, as the abstract frames it, is that a passing Lean check on an AI-made translation is not by itself grounds for confidence in the original natural-language argument. The full text is on arXiv, with a PDF and an experimental HTML version.

How solid is it

This account rests on the paper's abstract and submission page. The paper is a fresh arXiv submission (version 1, 6 October 2026), so it is a preprint, and no peer review or reply is mentioned. The abstract does not say whether the underlying natural-language Navier-Stokes proof is correct or incorrect; it only says the Lean version does not correspond to it. The abstract does not name the AI system or Lean version used for the translations, and does not say how many mistranslation examples there are beyond 'several'. The abstract does not say when OpenAI announced its proof, or whether OpenAI has responded.

Risks and caveats

The abstract says verification 'may' offer no confidence, not that it never does. The 'harder than the Halting problem' statement is an informal gloss ('informally'), not a formal theorem. The paper's finding is about a mismatch between the Lean and natural-language versions, and it should not be read as a verdict on whether OpenAI's natural-language proof is right or wrong. The abstract does not list the authors or their institutions; only the submitter name appears in the submission history.

“we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations”

— Abstract of the arXiv paper "Navier-Stokes lost in translation"