New Paper Says the Lean Proof of OpenAI's Navier–Stokes Result Doesn't Match the Written Proof: Passing a Machine Check Is Not the Same as Verifying the Argument

On October 6 Alexander Bastounis, Fabian Circelli and Anders C. Hansen submitted "Navier-Stokes lost in translation" (arXiv:2610.08144), using OpenAI's September Navier–Stokes blow-up result as an example of how AI mistranslates natural-language proofs into Lean, so that what passes the Lean check does not correspond to the written proof. The authors do not claim the result is wrong; their conclusion is narrower: a successful Lean check does not by itself establish the original written argument, and AI autoformalization needs additional semantic checking. According to TechCrunch, the paper documents at least two discrepancies between the written proof and the Lean code. The point also applies to the hundreds of math manuscripts OpenAI released on October 6, about 42% of which were formalized by TechCrunch's count.

What the paper says

In September OpenAI published a result on blow-up in the Navier–Stokes equations along with a Lean formalization; as this site reported at the time, it did not prove the classic version of the Millennium Prize problem. On October 6 Alexander Bastounis, Fabian Circelli and Anders C. Hansen submitted "Navier-Stokes lost in translation" to arXiv, with a subtitle that states the claim outright: Lean verification of AI autoformalization does not guarantee correct natural-language proofs.

The paper lists several cases where AI mistranslated natural-language statements and proofs into Lean, and OpenAI's Navier–Stokes result is one of them: the authors argue the formalized Lean proof does not correspond to the written blow-up proof. According to TechCrunch, the paper documents at least two such discrepancies.

What it doesn't say

The authors do not claim OpenAI's result is wrong. Their conclusion is narrower and more fundamental: Lean only checks the statement it is told to prove, so if the statement changed during translation, a passing check says nothing about whether the original written argument holds. The authors also argue, from a computational complexity perspective, that resolving ambiguity in mathematical text and translating it faithfully is extremely hard to fully automate, so AI autoformalization needs people to check meaning.

A caution for that batch of math manuscripts

The timing is pointed: on October 6 OpenAI released a batch of math manuscripts produced by an internal model, presenting partial Lean formalization as grounds for trust. By TechCrunch's count about 42% were formalized; TechCrunch also quotes Harvard mathematician Melanie Wood saying that at release no one truly understands the results yet, and that "the work begins" afterward.

That gives readers a concrete test: when you see "verified in Lean," ask exactly which statement was verified and whether it matches the paper's stated conclusion word for word. Until someone has done that check, there is still a step between "the machine checked it" and "the result holds."

via: arXiv paper, TechCrunch report