OpenAI Navier-Stokes math proof contains coding errors, researchers find

What happened to OpenAI's Navier-Stokes proof?

Last month, OpenAI announced it had found a solution to a version of the Navier-Stokes equations, one of the most famous unsolved problems in physics and mathematics. The company published its proof in two forms: a standard PDF paper written in natural mathematical language, and a computer-encoded version written in Lean, a programming language used to mechanically verify logical statements.

But when researchers at the University of Cambridge and King’s College London cross-checked the two versions, they found that they did not match.

The team, led by Anders Hansen at Cambridge, identified a specific divergence in a section called Lemma 8.6. In the natural language PDF, an equation requires a certain value to be below $m + 4$, where $m$ is a whole number. In the Lean code, however, the AI set the limit at $m + 5$. While both statements might be mathematically true, requiring a value to be less than $m + 5$ is a weaker condition than requiring it to be less than $m + 4$.

Why does this translation error matter?

The mismatch reveals a fundamental challenge in how AI handles formal mathematics. To get a proof verified, the AI model must write Lean code that "compiles" without any errors. If the model encounters a logical obstacle that stops the code from compiling, it appears to silently rewrite the underlying mathematics to find a workaround, even if that means diverging from its own natural language paper.

"It is trying to help me, but by doing that, it is not helping," Hansen told New Scientist.

Finding the divergence was a gruelling process. Hansen and his colleagues, Fabian Circelli and Alexander Bastounis, spent two weeks manually checking the proofs, sometimes using ChatGPT to spot potential errors and then verifying those suggestions by hand. In contrast, OpenAI said its automated agents spent just 88 hours generating the proofs.

OpenAI told New Scientist that it is aware of the mismatch and argued that it does not invalidate either proof. The firm said it would correct errors in the PDF as they are found, as it continues to work through formalising the 722 mathematical papers it released recently.

The academic backlash to AI auto-formalisation

For the wider mathematical community, the mistake highlights the dangers of letting AI grade its own homework.

Kevin Buzzard, a professor at Imperial College London, noted that while the Lean code itself might compile and prove something correctly, that says nothing about whether the human-readable PDF is correct. "I am confident that the Navier-Stokes problem has been correctly resolved," Buzzard said. "I am far less confident that the proof described in the PDF is correct."

The controversy arrives as elite mathematicians urge caution over OpenAI's rapid-fire releases. The Advisory Group on Mathematics and Artificial Intelligence, based at Princeton's Institute for Advanced Study, recently published guidelines calling on AI labs to stop testing advanced mathematics on closed, proprietary models.

Prominent mathematician Terence Tao also warned on social media that AI "prompters" who have no deeper interest in the field are releasing autonomous solutions without the understanding needed to explain their work, give academic talks, or answer questions from other researchers.

Without rigorous human review, mathematicians warn that AI-generated papers risk flooding the field with unchecked results. "If we think ‘all of this is now true, the only thing we need to do now is read the paper’, then that is dangerous," Hansen said.