---
id: "lib-2026-10-06-navier-stokes-lost-in-translation"
type: "library"
title: "Navier-Stokes lost in translation"
lang: "EN"
org: "Bastounis, Circelli, Hansen"
source_type: "Paper"
date: "2026-10-06"
week: "2026-W41"
url: "https://nosov.ai/library/lib-2026-10-06-navier-stokes-lost-in-translation/"
original_url: "https://arxiv.org/pdf/2610.08144"
tier: "A"
tier_name: "Strong evidence"
tier_reason: "Cambridge-led preprint (corresponding author Anders C. Hansen, DAMTP) giving concrete, checkable mismatches between OpenAI's Navier-Stokes paper and its Lean code plus a formal impossibility argument; not yet peer reviewed."
summary_basis: "full-text"
original_minutes: "60"
tags: ["ai technology", "formal verification", "lean", "ai for science"]
frames: ["verification-capacity"]
---

# Navier-Stokes lost in translation

Tier A (Strong evidence): Cambridge-led preprint (corresponding author Anders C. Hansen, DAMTP) giving concrete, checkable mismatches between OpenAI's Navier-Stokes paper and its Lean code plus a formal impossibility argument; not yet peer reviewed.

Summary based on the full text.

## In short

A. Bastounis, F. Circelli and A. C. Hansen argue that a Lean proof that compiles does not show that the natural-language proof it was "translated" from is correct. Using OpenAI's announced proof of finite-time blow-up for the Navier-Stokes equations, they show places where the Lean code proves a weaker or different statement than the paper claims. They add a logic result: faithfully resolving ambiguity in mathematical text is harder than the Halting problem. They make no claim about whether OpenAI's paper is right, only that Lean does not verify it.

## Key numbers

- m+4 vs m+5: derivatives required in OpenAI's paper (eq. 8.19) versus in the cited Lean theorem
- SCI = ∞: complexity of resolving ambiguities for faithful autoformalisation, versus SCI = 1 for the Halting problem
- 13 million: lines of Lean in Anthropic's Fermat's Last Theorem autoformalisation, cited as a scale problem for checking

## What it reports

- Two kinds of autoformalisation: (i) turning a proof into any Lean proof that compiles; (ii) faithfully translating every statement and argument. Success at (i) says nothing about the original text.
- Example 2.1: ChatGPT-6 (Astra Ultra) turned a wrong proof (wrong root multiplicities) into a correct Lean proof.
- Example 2.2: a correct diagonalisation proof became a different correct Lean proof that skips the change of basis.
- Example 3.1: OpenAI's Lemma 8.6, eq. (8.19), bounds output derivatives with m+4 input derivatives; the cited Lean theorem (commit f9e8bc5) needs m+5, a strictly weaker result. The mismatch recurs across the code.
- Example 3.3: the pressure-flux bound (10.19) and its proof are both replaced by a different bound and argument in Lean.
- The authors expect "substantial mistranslations" in OpenAI's companion Euler proof too, based on preliminary checks.
- They cite Meta's spring 2026 claim of 26 textbooks autoformalised (45,000 declarations, about 500,000 lines), which Lean experts rejected after finding fatal errors.

## How they got it

Manual line-by-line comparison of the OpenAI paper and its GitHub Lean code, chatbot experiments, and a proof placing ambiguity resolution in the Solvability Complexity Index hierarchy via Hilbert's 10th problem.

## Limits

- Only two Navier-Stokes examples are worked in detail; the Euler claim is a prediction.
- Preprint, not yet peer reviewed; the impossibility result is about worst-case general guarantees.

## Why it matters for companies

The same logic applies to any "AI-verified" output: a passing test or compiled check confirms the check, not that the original reasoning or specification was preserved. When an agent is rewarded only for passing, it can quietly change the problem. Review needs a step that compares what was asked with what was actually proved, built, or tested.

Original: https://arxiv.org/pdf/2610.08144