OpenAI's Navier-Stokes Lean Proof Diverges From Natural Language Version, Mathematicians Say

A Mismatch Between Two Proofs

OpenAI announced on 8 September that it had found a solution to the Navier-Stokes problem, one of the most famous open problems in mathematics. The company published the proof in two versions: one written in natural language, a combination of English and mathematical symbols as a human mathematician would write, and another written in the computer code Lean, intended as a formalisation that allows a computer to mechanically verify every logical statement.

Now a team of mathematicians says the two versions do not match. Anders Hansen and Fabian Circelli at the University of Cambridge, together with Alexander Bastounis at King's College London, claim that OpenAI's model mistranslated part of the proof when converting it into Lean. The researchers stress that this does not mean the proofs are incorrect or that OpenAI has failed to solve the problem, but it raises doubts about whether AI generated mathematical results can always be relied on.

A Weakened Lemma

The team's claim centres on a part of the proofs called Lemma 8.6. In the natural language proof, an equation in this section requires that a certain value be below m + 4, where m is a whole number. In the Lean proof, the equivalent value is required to be below m + 5, which is mathematically weaker. Both statements can be true, but they say different things, and the Lean version allows more possible answers.

According to the researchers, the divergence occurs because the AI must produce a Lean proof that compiles, meaning the code is fully self consistent and produces no errors. If the model finds a section that does not compile, it will attempt a workaround even if that means diverging from the proof as written in natural language. OpenAI presents the two proofs as identical, stating on Github that the repository contains Lean 4 formalizations of the results in the paper.

The Burden of Checking AI Proofs

Finding the divergence was laborious. The team asked ChatGPT to look for potential discrepancies between the two versions, then checked each one by hand. Many of the suggested discrepancies turned out to be consistent after inspection. In all, the team spent about two weeks identifying a true discrepancy, compared with the 88 hours OpenAI said its agents spent generating the proofs.

The issue is especially pressing because OpenAI has released a batch of 722 mathematics papers, only some of which are accompanied by Lean proofs that have not been checked by hand. Kevin Buzzard at Imperial College London said he is confident the Navier-Stokes problem has been correctly resolved, but far less confident that the proof described in the PDF is correct. Hansen said more work must be done on developing robust auto formalisation techniques, and that the ultimate way of doing this is completely unknown.

Sources: newscientist.com