Paper flags gap in OpenAI's Lean-verified Navier-Stokes proof

OpenAI's announced Lean proof of blow-up of solutions to the Navier-Stokes equations does not correspond to the natural-language argument it was meant to formalise, according to an arxiv preprint posted October 6 by Alexander Bastounis, Fabian Circelli and Anders C. Hansen.

The abstract states it plainly: "the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations." Two of the mathematicians we track have already passed the link around.

The authors' broader argument is theoretical. They place the problem of resolving ambiguities needed for a semantically faithful translation from mathematical English into Lean "arbitrarily high up in the Solvability Complexity Index (SCI) hierarchy," and conclude that, informally, "providing semantically faithful AI autoformalisation is harder than any computational problem including the Halting problem (which has SCI = 1)."

To ground the result in current practice, they add "several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean 'verifications'." The Navier-Stokes case headlines the set. The abstract names no specific Lean file, no commit hash, and no accuracy rate across the examples.