OpenAI's Navier-Stokes Proof Has a Translation Problem
Original: Navier–Stokes Lost in Translation
Why This Matters
Formal verification is gaining traction as the gold standard for AI-generated math proofs.
Researchers at Cambridge argue that OpenAI's AI-generated Navier-Stokes proof, verified in Lean, may not match its natural language claims—because faithful autoformalisation is computationally harder than the Halting problem.
A 25-page paper by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen (arXiv:2610.08144) takes direct aim at a central assumption behind AI-assisted formal math: that a Lean-verified proof is a verified proof. The authors argue it isn't—at least not necessarily.
The problem is autoformalisation, the process of translating natural language (NL) math into a formal language like Lean so it can be mechanically checked. OpenAI used this approach for its announced proof concerning blow-up of solutions to the Navier-Stokes equations. The paper claims that the Lean formalisation does not actually correspond to the NL proof OpenAI presented.
The theoretical core is stark: resolving semantic ambiguities in mathematical NL text—required for any faithful translation—sits arbitrarily high in the Solvability Complexity Index (SCI) hierarchy, with SCI = ∞. That places it beyond the Halting problem (SCI = 1). In other words, no algorithm can reliably do it.
The authors back this up with concrete examples of AI mistranslations of NL statements and proofs into Lean, showing real-world mismatches between what a proof says and what gets formally verified. The implication: a green checkmark in Lean may say nothing about whether the underlying mathematical argument is correct.