A preprint posted Oct. 6 says the Lean code OpenAI published for its claimed Navier-Stokes result does not faithfully match parts of the written argument. The authors point to an estimate where the code requires one more derivative of smoothness than the paper does.
Lean is a proof assistant: it checks whether a formal statement follows from steps encoded in Lean. That check applies to the statement in the code. It does not, by itself, show that the code expresses exactly what a paper says.
The preprint's example is Lemma 8.6. OpenAI's paper says the estimate needs m+4 derivatives of its input to establish a result with m derivatives. In the corresponding theorem in the Lean source at the commit cited by the authors, the input requires m+5 derivatives. That extra derivative is a stricter smoothness requirement, so the two statements are not identical. The authors trace this to how each proof controls the same mathematical series: the paper's bound works with four extra derivatives, while the Lean version's bound requires five.
The authors explicitly say they are not claiming OpenAI's natural-language proof is false. Their narrower claim is that the cited Lean formalization does not faithfully encode parts of the written argument. The work is an arXiv preprint, not a peer-reviewed verdict. OpenAI's Sept. 8 announcement described its analytical proof and Lean formalization as resolving the Navier-Stokes problem.
For AI-assisted mathematics, the review therefore has two parts: check the Lean proof, and check that Lean is proving the same statement as the paper.
Image: Lorenzo Cafaro, “Programming.jpg” via Wikimedia Commons, CC0 1.0. Illustrative sample-code screen.
Related coverage: OpenAI's release of 722 AI-generated math manuscripts.
Sources
The preprint; OpenAI's paper; the cited Lean source revision; OpenAI's announcement.