What happened: Three analysts at King’s College London and Cambridge compared the natural-language manuscript of OpenAI’s announced Navier–Stokes blow-up proof with the Lean declarations cited as its verification, “at commit f9e8bc5”, and display two places where they part. At Lemma 8.6 the text’s estimate loses four derivatives and “the related Lean codes – on the other hand – all use five additional derivatives, not four”, so the Lean result is weaker than the sentence it is said to certify; at the pressure-flux bound the method and the quantities differ and “the two bounds … are therefore hard to compare.” Behind the two cases sits a result about the method: resolving the ambiguities of mathematical prose is placed at infinity on the Solvability Complexity Index hierarchy, so that a faithful autoformaliser is “harder than any computational problem including the Halting problem.” The conclusion is bounded in the authors’ own words — “The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments. Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean” — and the recommendation follows: such proofs “should not prima facie be trusted without the same peer review process and scrutiny that other proofs are subjected to.” Two other readings of the same manuscript arrived in the same fortnight. Lei and Ren at Fudan give “a readable and accessible version of the profile-construction part” and “regard OpenAI’s work as a major advance on the Navier–Stokes Millennium Prize Problem”; Gamburd, in an essay now at its third version, sets a certificate of truth against a demonstration that lets another see why, and asks what is accepted when the first arrives without the second.
Diagnostic reading: The pre-registration (2026-08-29-prereg-attribution-mathematics) committed in advance to watching two registers at once — what is said about the artefact and what is said about its producer — on the expectation that the first would hold while the second moved. This entry records the first register doing something the design did not anticipate: splitting. “Verified” has come apart into theorem verified and proof verified, and the three readings distribute themselves across the gap. Lei and Ren reconstruct the argument so that a reader can follow it, which is Gamburd’s demonstration supplied by hand; Bastounis, Circelli and Hansen show that the certificate does not reach the argument it was taken to cover; Gamburd names what is at stake if the field settles for the certificate. None of the three disputes the Lean. For ARG-03 v2.6 §5 this is the provenance register working exactly as that section says it can: the question of where a result came from and whether its stated route is the one taken is investigable, and here it is being investigated lemma by lemma by people with no access to the producer — while the authorship question the same section holds to be unverifiable in principle is not touched by any of them, and could not be. The symmetry test (ARG-01 v1.5) is passed by the method and the entry records it as passed: the scrutiny proposed is “the same peer review process … that other proofs are subjected to”, applied because the proof was autoformalised and not because a machine wrote it, and the toy examples run the same mistranslation on human-written text. What the three readings do not do is ask the reciprocal question — what a human author of a correct theorem with an unreadable proof would be owed — and the entry marks that as the gap the window’s later readings will need. On the pre-registration’s direction axis nothing moves: no criterion for the artefact has been loosened or tightened, and the figure caption in which a frontier model “shares our concern” about its rival’s translation is recorded as a curiosity of the period rather than a datum. What the split does to the attribution question is the open item. A result certified to a machine and demonstrated to no one is the knowing-as-configuring question (ARG-03 v2.6 Part II) seen from the receiving side; these papers are the receiving side at work, and they are the first evidence in the window that the field’s answer will be to do the demonstrating itself. [Derived]
Preprint (arXiv:2610.08144v1 [math.AP], 6 October 2026, 25pp), read in full from the arXiv HTML 2026-10-15, quotations verified; Gamburd (arXiv:2609.28591v3, 1 October) and Lei & Ren Part I (arXiv:2609.35406v2, 29 September) likewise. OpenAI's manuscript and Lean repository are not held and nothing from them is quoted; what the entry says about them is what the three readings say. The authors state a prior position (Hansen's Solvability Complexity Index programme) and their toy examples are constructed; neither touches the disclaimer-bounded finding. Nothing here bears on whether the blow-up theorem is true. The pre-registration this entry points back to is never edited; this is an interim reading in its window, not its outcome.