When OpenAI announced its surprise solution to the Navier-Stokes problem, it produced one proof for humans and one for computers – however, they don’t match.
OpenAI appears to have made a subtle error when publishing its proofs of the Navier-Stokes problem, a team of mathematicians has claimed. The error doesn’t mean that the proofs are incorrect or that OpenAI hasn’t correctly solved the problem, but it does call into question whether mathematical results generated by AI models can always be relied on.
“What has to be done with all of these large language model-generated proofs is that they will have to be read by humans, and this creates an enormous extra burden on mathematicians,” says Anders Hansen at the University of Cambridge.
On 8 September, OpenAI announced that it had found a solution to the Navier-Stokes problem, one of the most famous open problems in mathematics. It published the proof in two versions – one written in “natural language”, meaning a combination of English and mathematical symbols, as a human mathematician would write, and another written in the computer code Lean. The Lean proof is meant to be a formalisation of the natural-language version, allowing a computer to mechanically verify that all of its logical statements are true. The problem is, say Hansen and his team, that they don’t match.
“This formalisation process is trying to replace peer review,” says team member Fabian Circelli, also at the University of Cambridge. “Peer review would mean that human eyes look at the proofs. But what we’ve shown in this paper is that using this type of AI auto-formalisation can’t serve the same purpose.”
To be clear, the researchers aren’t saying that OpenAI has failed to solve the Navier-Stokes problem. It is entirely possible that both the natural-language proof and the Lean one provide a solution, just as there are hundreds of valid proofs of Pythagoras’s theorem. Instead, their point is a more subtle one: that OpenAI’s model has “mistranslated” when converting into Lean.
The team’s specific claim hinges on part of the proofs called Lemma 8.6. In the natural-language proof, an equation in this part 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.
OpenAI told New Scientist that it is aware of the mismatch between the natural-language proof and the Lean code, and that this doesn’t mean that either proof is invalid. It says it will rectify any errors in the natural-language proof as they are found, and will also continue the process of formalising the 722 maths papers the firm released this week, only some of which are accompanied by Lean proofs, which themselves haven’t been checked by hand.
Finding the divergence involved asking ChatGPT to look for potential discrepancies between the natural-language and Lean proofs, then checking them by hand. In all, it took the team about two weeks to identify a true discrepancy, compared with the 88 hours OpenAI said its agents spent generating the proofs.
Kevin Buzzard at Imperial College London notes that in discussions like these, it is important to distinguish between the statement of a theorem and its proof. “I am confident that the Navier-Stokes problem has been correctly resolved,” says Buzzard. “I am far less confident that the proof described in the PDF is correct.”
Hansen says he hopes OpenAI will take the team’s work “very seriously” and that more work must be done on developing robust auto-formalisation techniques.