Abstract
This study presents an independent critical audit of OpenAI's 166-page proof Finite time blowup for Navier–Stokes, its associated public Lean formalization, and the claim-level correspondence with the Clay Mathematics Institute's (CMI) C/D alternatives. The purpose of the audit is not to assign a subjective percentage of correctness to the proof; its task is to separate and examine four mutually independent evidentiary layers: (1) the analytical proof architecture and high-risk PDE nodes; (2) traceability from the PDF to the formal source/module/declaration chain; (3) source/type and mathematical-semantic consistency between the Fefferman C/D formulation and the final Comparator theorem types; and (4) the independent execution status of a clean, reproducible kernel/Comparator/Nanoda replay. The review covers all ten chapters of the paper, Appendices A–C, and 65 numbered subsections, while the referee-oriented deep audit concentrates on Theorem 4.6, Lemma 5.4, Proposition 9.6, Proposition 9.9/Lemma 9.8, Lemma 10.3, and Lemma 10.5. The results substantially narrow, but do not close, the uncertainty surrounding independent certification. Selective algebraic, scaling, energy, residual-closure, and functional-analytic consistency checks found no specific fatal contradiction/counterexample in the audited subclaims. Critical-node traceability from six high-risk PDF nodes to the final C/D endpoints has been established; no material weakening was found in the source/type + semantic comparison of Fefferman's quantifier order, admissible data/forcing classes, smoothness/decay, bounded-energy, and periodic-pressure requirements. These findings, however, are deliberately not relabeled as a universal lemma-by-lemma PDF↔Lean concordance or as a kernel-checked formal equivalence proof. In particular, the full quantitative dependency tree of Theorem 4.6, every weighted/support estimate in Lemma 5.4/Proposition 9.9, the complete term-class calculus of Proposition 9.6, and every distributional/commutator passage in Lemma 10.5 have not been independently discharged line by line in this report. The clearest boundary of formal verification is the independent replay: in the current environment the required toolchain/transport prerequisites could not be satisfied, and `lake build`, final `#print axioms`, Comparator, and Nanoda proof stages were NOT REACHED; consequently, neither independent replay success nor proof failure has been established. OpenAI's first-party Lean verification assertion and public formalization metadata constitute an important evidentiary layer, but they cannot replace a third-party, hash-pinned, exit-0 kernel certificate. The CMI's Qualifying Outlet requirement, the minimum two-year period, and general acceptance are additional external procedural gates. Accordingly, the final conclusion of this audit is strictly two-part: OpenAI's resolution claim has strong positive source/structural and semantic evidence, and no fatal defect was identified within this scope; but complete independent mathematical certification still lacks decisive line-by-line PDE referee discharge, kernel-checked specification equivalence, and a reproducible exit-0 independent replay.
Showing the abstract — retrieve the full paper via the Exa API.