A preprint submitted October 6 by Alexander Bastounis, Fabian Circelli and Anders C. Hansen challenges the relationship between a natural-language mathematical argument and a Lean formalization presented as its formal verification. The authors argue that the formalized proof associated with OpenAI's announced work on Navier–Stokes blow-up does not correspond to the argument written in natural language.
The distinction matters because a proof assistant checks the formal statement it receives. Before that can happen, an autoformalization system must translate ordinary mathematical prose into definitions and claims expressed in a formal language. A mechanically valid Lean proof shows that the formal version follows from its stated premises, but it does not by itself establish that the translation preserved the meaning of the original text.
Where verification can diverge
The authors argue that ambiguity in mathematical language makes faithful translation unusually difficult. Their paper places the problem of resolving those ambiguities arbitrarily high in the Solvability Complexity Index hierarchy and informally describes semantically faithful autoformalization as harder than any computational problem, including the Halting problem. That is the authors' theoretical claim in a new preprint, not an independently established verdict on OpenAI's underlying mathematics.
To illustrate the practical risk, the paper says it found several cases in which AI translations of natural-language statements and proofs into Lean produced meanings that did not match the original prose. Its examples include the announced Navier–Stokes argument, for which the authors say the verified formal proof and written proof do not correspond. The issue they identify is therefore not that Lean incorrectly checked a formal proof, but that the formal object may not represent the intended claim.
