OpenAI's Lean code for its Navier-Stokes proof loosens a bound set in the written paper

The looser bound matters because a weaker inequality proves less. New Scientist gives a schoolroom version: if x + 3 = 6, it is true that x is less than 4 and also true that x is less than 5, but the second statement admits more answers ^[5]. A proof built on the weaker step can still reach a valid result ^[9]. At that step, though, it is a different proof from the one on paper ^[4].

Hansen said the gap comes from what the formalising model is required to produce ^[7]. Its Lean has to compile, meaning the code is self-consistent and returns no error. When a section of the written argument will not compile, the model looks for a workaround, even one that departs from the paper ^[7]. Lean then checks the statements in the code it was given, workaround included ^[2].

The team's claim is narrow, and Hansen set its limits himself ^[3]. "We are not saying that the natural-language proof is wrong," Hansen said. "Nor do we say that it is correct." ^[8] Both versions could solve the problem, in the way Pythagoras's theorem has hundreds of valid proofs ^[9]. The objection is to the label. OpenAI's GitHub repository says it "contains Lean 4 formalizations of the results presented in" the paper "Finite time blowup for Navier-Stokes" ^[6]. At Lemma 8.6 the code formalises a weaker statement than the paper makes ^[4].

Finding the mismatch took far longer than producing the proof. The team needed about two weeks to identify one true discrepancy, against the 88 hours OpenAI said its agents spent generating the proofs ^[14]. Two weeks of calendar time is 336 hours, about 3.8 times the agent figure ^[18]. The two numbers are in different units, a team's elapsed time set against a machine total that OpenAI supplied, so the ratio is rough. "Going through all of these things manually was a nightmare," Hansen said ^[13]. "OpenAI boast about how quickly they were able to generate this result, but that's only part of the process," said Alexander Bastounis of King's College London, a member of the team ^[15].

"This formalisation process is trying to replace peer review," said Fabian Circelli, also of Cambridge ^[10]. "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." ^[10] I think the evidence supports a slightly narrower version of that. On this paper, the Lean check did not do a reviewer's job, and it took a hand check of machine-flagged candidates to show it ^[12]. So far the team has reported one true discrepancy, in one lemma ^{[4] [14]}.