Researchers examining OpenAI’s AI-generated Navier-Stokes work have identified a gap between its written proof and the Lean artifacts cited as verification. Their criticism concerns whether the two express the same mathematics, even if the formal code passes Lean’s mechanical checks.
In the October 6 preprint, Alexander Bastounis, Fabian Circelli, and Anders C. Hansen argue that OpenAI’s cited Lean formalization does not faithfully establish its written proof of blow-up for solutions to the Navier-Stokes equations. They identify translation mismatches, including differences in conditions and mathematical arguments. They do not claim that OpenAI’s natural-language proof is incorrect.
Formal verification is a powerful trust signal for AI-generated mathematics. According to TechCrunch’s October 8 report, OpenAI released 719 mathematical manuscripts that week. At that scale, readers need to know whether a successful formal check validates a theorem, the published reasoning, or both.
The preprint also gives a concrete technical rationale for mathematicians’ recent responsible-release guidelines, which call for explicit connections between written proofs and their formal counterparts.
Lean Checks the Formal Argument It Receives
Lean is a proof assistant: it checks a mathematical argument expressed in a precise formal language. That precision removes much of the ambiguity in ordinary mathematical writing, where authors routinely leave definitions, dependencies, and intermediate reasoning implicit. The checking happens after someone, or something, has translated the mathematics into Lean.
The preprint distinguishes two tasks that are easy to conflate. In the first, a theorem statement has already been faithfully formalized, and an AI system must produce a Lean proof of it. In the second, the system must faithfully translate an entire mathematical text, preserving its definitions, theorem statements, intermediate results, and arguments.
Success at the first task does not establish success at the second. A model can produce a valid proof of a correctly stated theorem while abandoning the reasoning it was asked to translate. It can also formalize a different statement whose proof is easier to complete.
Lean’s checking is not being called unreliable here. The formal system evaluates the mathematical content encoded in the artifact. It does not independently compare that content with an external manuscript and certify that the translation preserved its meaning.
The authors make this point even under a demanding success criterion: Lean code that compiles without using the sorry placeholder or introducing extra axioms. Removing such shortcuts strengthens confidence in the formal proof, but the correspondence between that proof and its source text still needs to be established.
For readers, “Lean-verified” therefore needs an object. Which statement was verified, under which assumptions, and how does it relate to the published manuscript?
The Navier-Stokes Criticism Concerns Both Statements and Reasoning
The researchers apply this distinction to OpenAI’s announced Navier-Stokes blow-up argument. They argue that the cited formalization does not correspond faithfully to the natural-language proof it is presented as verifying.
The reported mismatches involve two separate issues: formal statements that impose stronger conditions than their natural-language counterparts, and formal proofs that use different mathematical arguments.
The first concerns the scope of a result. As a general illustration, a written theorem might assert that a conclusion follows under assumption A, while its formal counterpart establishes the conclusion only under A plus an additional assumption B. A correct proof of the second statement does not, by itself, prove the first. It covers a more restricted set of cases.
This illustration does not reconstruct OpenAI’s equations. It explains why differences in hypotheses have mathematical consequences and cannot be treated as cosmetic translation choices.
The second issue concerns the route to the conclusion. A formal proof might establish a theorem through another argument, without validating the manuscript’s intermediate claims or deductions. That can be valuable mathematics, but it is a different achievement from checking the written proof.
Establishing a formal theorem, faithfully translating a theorem statement, and faithfully verifying a published argument are related accomplishments. They are not interchangeable, and a release’s description should distinguish them.
The authors’ disclaimer is essential here. A failure to establish correspondence does not demonstrate that the original argument is false. It shows that the formal artifact cannot bear the particular evidentiary weight assigned to it: certifying the correctness of that argument.
The critique is itself an arXiv preprint and should be evaluated through mathematical scrutiny. Its publication is not a final adjudication of OpenAI’s work.
A Correct Replacement Proof Can Hide a Translation Failure
The paper’s elementary examples make the problem easier to understand without requiring expertise in fluid dynamics.
In the preprint’s worked examples, the authors present an intentionally incorrect natural-language proof about the polynomial:
p(x) = x³ − x² − x + 1
The conclusion is that the polynomial is nonnegative for x ≥ −1. That conclusion is correct, but the supplied argument assigns the wrong multiplicities to the polynomial’s roots and consequently gives an incorrect factorization.
The correct factorization is:
p(x) = (x + 1)(x − 1)²
On the stated domain, the first factor is nonnegative and the second is a square.
When asked to translate the erroneous argument into Lean, the AI produces a correct formal proof by repairing the mathematics. The resulting artifact is useful as a proof of the conclusion. It provides no evidence that the original reasoning was correct, because the system replaced the faulty step.
A second example shows that translation can fail even when nothing needs repairing. The natural-language argument establishes that the trace of the square of a real symmetric matrix is nonnegative. It does so by diagonalizing the matrix and expressing the result as a sum of squared eigenvalues. The AI’s formal proof instead works directly with matrix entries, using symmetry to obtain a sum of squares.
Both arguments are correct. They are nevertheless different proofs.
The question, then, extends beyond whether AI-generated mathematics is right or wrong. A translation can be unfaithful while producing a valid theorem and a valid proof. If the intended task was to verify the source argument, correctness of the replacement does not complete that task.
There are legitimate reasons to prefer an alternative proof during formalization, including a better fit with available formal results. Readers should be told when the formal artifact establishes the conclusion by another route, so they do not mistake it for a check of every step in the manuscript.
Responsible-Release Guidelines Ask for the Missing Connection
The Advisory Group on Mathematics and Artificial Intelligence anticipated this need in its September 29 responsible-release recommendations.
For AI-generated results that nobody yet fully understands, the group recommends releasing the model’s identity, prompts, summarized reasoning, time taken, and estimated computational cost. It also asks labs to state formalization status clearly and, where possible, provide formal artifacts meeting community standards.
