OpenAI’s Navier–Stokes proof has a translation problem, researchers say

Researchers at King’s College London and the University of Cambridge say OpenAI’s human-readable proof of a Navier–Stokes result does not fully match the version checked in Lean, a system for verifying mathematical proofs. Their finding raises a pointed question about what computer verification actually confirms: the code’s logic, or the proof people are being asked to trust?

OpenAI Watch analysis

What happened

In a preprint published on 27 October, the researchers report several discrepancies between OpenAI’s two versions of its proof. In one example, the written proof makes a stronger claim than the corresponding Lean version. The preprint has not been peer-reviewed.

The researchers do not say that OpenAI’s original proof is wrong, or that its claimed mathematical result is false. Their finding is narrower: a logically valid Lean proof does not establish that it faithfully represents the separate argument written for mathematicians.

Why it matters

Formal verification can check whether a proof follows from its stated assumptions. But if the formal version and the human-readable one make different claims, checking one does not automatically validate the other. The translation between them is part of the trust problem, not a clerical detail to wave away.

That matters beyond this particular result. As AI systems produce mathematical arguments, researchers need ways to scrutinise both the reasoning and any conversion into machine-checkable form. The authors also argue that there is no general automatic method for translating every human-written mathematical argument into a formal proof.

Our read

This is a challenge to the link between two versions of a proof, not a verdict that OpenAI’s result is incorrect. That distinction is important, and rather less tidy than a simple “the computer checked it” headline. The useful test is whether the mathematical argument can be examined on its own and shown to match the formal one.

What to watch

• Whether OpenAI or other researchers respond to the specific discrepancies.
• Whether the preprint’s findings change after peer review or further scrutiny.
• What methods researchers develop to check that formal proofs faithfully represent human-readable arguments.

Discussion spark: Should a machine-checked proof count as strong evidence when its human-readable counterpart has not been shown to make the same claims?

OpenAI Watch is independently operated by WittyWires. It is not affiliated with, endorsed by, or operated by OpenAI.