Researchers find discrepancies in OpenAI's Lean proof on Navier–Stokes

Researchers compared OpenAI's published proof on the Navier–Stokes equations with its formalized Lean version and found discrepancies at several key points. At those points, the machine-checkable version proves weaker claims than the ones stated in the text for human readers. The Navier–Stokes equations are one of the seven Millennium Prize Problems of the Clay Mathematics Institute, each carrying a prize of 1 million dollars, so any crack in such a result gets noticed immediately. This is not a refutation, at least not yet.

What exactly was found

The check itself is simple. Take the paper with the proof and, alongside it, the formal version written in Lean, a language in which a computer verifies every step of the reasoning. If both versions describe the same thing, they match. Here they did not: at several pivotal points, the Lean version claims less than the text.

The description of the check does not say whether OpenAI's work claims a full solution of the Clay problem or a narrower result. The scale of the claim has to be judged from the publication itself, and that is an important caveat. But it does not change the conclusion: the formal artifact must match what the paper promises.

Why a "weaker claim" is serious

Lean does not accept arguments like "this is obvious" or "it follows from standard considerations." If a proof passes verification, it is correct relative to what is actually written in the formalization. So the key question is whether the formal version proves the same thing that the prose asserts. When the statement in the code is weaker than the one in the paper, several scenarios are possible:

• the formalizers simplified the conditions to get the work finished and did not say so;
• the theorem is stated imprecisely in the text, and the Lean version shows what was actually proved;
• a step that looks proved in the paper does not hold up under strict verification;
• the discrepancy comes from a technical mismatch in definitions that a fix would resolve.

The first and fourth scenarios are harmless; the third is dangerous. Until the authors or independent experts go through each point individually, there is no way to choose among them.

Key facts from the available information:

• subject of the check: OpenAI's proof on the Navier–Stokes equations;
• method: comparing the published text with the algorithmic Lean version;
• result: discrepancies at several key points;
• nature of the discrepancies: the claims in the machine version are weaker;
• status: this is not yet a refutation, but it is grounds for doubt.

What to watch next

If you follow AI in mathematics, a few markers are worth keeping in mind. First, OpenAI's response. A clear account of each discrepancy, whether a corrected statement, updated Lean code, or an acknowledgment of limitations, will say more than any general statement. Second, what specialists in fluid dynamics and partial differential equations say. Formal verification checks logic, but only domain mathematicians can judge whether the meaning of the problem got lost along the way. Third, whether the formalization and supporting materials will be published, so that the check can be reproduced independently.

For those who make decisions based on claims like this, the takeaway is practical. An AI result in mathematics should be considered confirmed when there is independent verification and the formal version matches the stated theorem. A press release and a preprint are not enough. Until the discrepancies are resolved, the Navier–Stokes story remains a loud claim, not an accepted fact.