Navier–Stokes Lost in Translation: Smooth External Forcing, the Lemma 8.6 Derivative Mismatch, and the Epistemological Limits of AI Autoformalisation

On September 8, 2026, OpenAI announced a 166-page manuscript establishing finite-timeblow-up for the three-dimensional incompressible Navier–Stokes equations with smooth externalforcing, accompanied by a machine-checked formalization in the Lean 4 theoremprover. While the announcement was widely publicized as a resolution of the Clay MathematicsInstitute’s Millennium Prize Problem, the mathematical community has raised twofoundational objections. First, from the standpoint of partial differential equations and fluidmechanics, OpenAI’s construction addresses the externally forced problem variants (ClayStatements C and D) rather than the unforced physical equations (Statements A and B), relyingon an implicitly constructed, non-analytic C∞ forcing profile to cancel singular momentumresiduals. Second, from the standpoint of formal verification, an October 6, 2026 auditby Bastounis, Circelli, and Hansen (arXiv:2610.08144 ) demonstrated that OpenAI’s compiledLean repository (commit f9e8bc5) does not faithfully translate the natural-languagemanuscript. In particular, Lemma 8.6 in the written paper claims control of the torus directionalinverse operator N−1 using m + 4 input derivatives, whereas the correspondingLean theorem requires m + 5 derivatives, and the uniqueness argument in Equation (10.19)is replaced by a substantively different inequality in code. This paper provides a rigoroustechnical examination of both controversies and assesses their implications for MillenniumPrize adjudication and mathematical peer review.