OpenAI’s Navier-Stokes proof called into question

The Navier-Stokes equations help describe how fluids such as water and air move, but have puzzled mathematicians for centuries. Solving them would be a significant mathematical achievement.

In a new pre-print, King’s College London and the University of Cambridge mathematicians discovered that the version of OpenAI’s Navier-Stokes proof written in a programming language designed to verify mathematical proofs does not fully match the proof published for human mathematicians.

While the finding does not yet establish that OpenAI’s original proof is incorrect, or that its claimed mathematical result is wrong, it suggests that the written proof and its computer-verified version make different mathematical claims. This means that verifying the formal version alone cannot establish that the original written proof has been correctly represented and checked.

Dr Alexander Bastounis, co-author of the paper, and Lecturer in Applied Mathematics, King’s College London, said: “OpenAI’s struggle to accurately translate its proofs into a machine-checkable language highlights a broader challenge: verifying the correctness of the output of an AI remains exceptionally difficult.”

The research is reported in a preprint published on arXiv. The paper has not yet undergone peer review.

In September 2026, OpenAI announced that its AI systems had produced a proof showing that such a breakdown can occur under certain conditions, addressing the longstanding mathematical problem.

The company published two versions of its proof: one written in conventional mathematical language and notation, and another in Lean, a programming language used to check mathematical arguments.

Mathematical proofs do more than establish whether a result is true. They explain why it is true, allowing other researchers to understand the reasoning, develop new techniques and build further work on the results.

Lean can verify whether a formal proof follows logically from its stated assumptions. However, this does not automatically establish that a separate proof written in conventional mathematical language makes the same mathematical claims. Computer verification can establish whether a written proof is correct if that proof has been correctly translated into a formal language. The challenge is establishing that the translation is accurate. Lean code is designed primarily to enable machines to verify mathematical arguments, making it unsuitable for mathematicians to readily scrutinise the reasoning or use the results in their own research. Researchers therefore need to be able to scrutinise the original mathematical argument, as well as establish that any computer-verified version faithfully represents it.

Drawing on their work investigating the limitations of AI, the researchers questioned whether OpenAI’s written proof had been translated accurately into Lean.

When the researchers compared the two versions of OpenAI’s proof, they found several places where they did not match. In one example, the written proof makes a claim that is stronger than the corresponding claim in the computer-checked version. In other words, the two versions do not quite say the same thing.

The researchers have not shown that OpenAI’s original proof is wrong. Instead, their findings show that a computer confirming that a Lean proof is logically correct does not guarantee that the Lean proof matches the argument written for mathematicians to read. The written proof still needs to be checked independently to establish whether its reasoning is correct.

Their analysis also reveals a deeper problem: there is no general way to automatically translate mathematical arguments written for humans into a form that computers can verify. The researchers used a mathematical framework called the Solvability Complexity Index (SCI) hierarchy, which helps classify computational problems according to how they can be solved by computers, including whether they can be solved using a reliable, step-by-step process. Their findings reveal a fundamental limit to automatically translating mathematical arguments written for humans into proofs that computers can verify.

Fabian Circelli, co-author of the paper, and PhD researcher at the University of Cambridge, said: “Our paper uses tools from the SCI hierarchy and logic to prove fundamental limits on what any AI autoformaliser can do, allowing us to predict the difficulties that AI autoformalisation will – and does – face in practice.”

As AI systems become increasingly capable of producing mathematical results, the researchers say it will be important to develop reliable ways of checking both the proofs themselves and the process by which they are translated into formal languages. Their findings highlight a fundamental limitation of relying on automatic translation to bridge the gap between mathematical arguments written for humans and formal proofs designed for computers.

Professor Anders Christian Hansen, co-author of the paper, and Professor of Mathematics at University of Cambridge, said: “The study demonstrates just how crucial the foundations of computational mathematics are for understanding the capabilities and limitations of AI.”