An independent rebuild, kernel replay and statement audit of the openai/NavierStokesAndEuler breakdown theorems (independently rebuilt and audited; not a claim that a Clay problem is solved)

OpenAI published a Lean 4 corpus, openai/NavierStokesAndEuler, whose authors present it as formalizing finite-time blowup results: for every positive viscosity, alternatives (C) and (D) of the Clay Institute's Navier–Stokes problem description (C. L. Fefferman), and a finite-time singularity for the unforced Euler equations. This record independently (of the corpus authors) rebuilds and audits that corpus, and was itself audited by a separate AI agent instance (verdict ACCEPT_WITH_CORRECTIONS; corrections applied). It does not claim that any Clay problem is solved; credit for the proofs belongs to the corpus authors, and the Clay Institute's own process decides any prize. What was done and found. At corpus commit f9e8bc5b, with the corpus's own toolchain (Lean 4.34.0-rc2) and a reused exact-revision Mathlib (85e3a25e), all 2,440 corpus modules were rebuilt from source (609 + 1,829 solution-closure modules and 2 challenge modules; rc 0; zero warnings in the two solution builds). The four theorems navier_stokes_breakdown_R3, navier_stokes_breakdown_periodic, euler_breakdown_R3 and exists_compact_smooth_euler_singularity depend on exactly [propext, Classical.choice, Quot.sound] in the author's own audit files. Source scans of 2,585 closure modules and all 2,659 corpus files and an environment scan of the proof closures found no soundness escape, and every scan caught its planted negative controls. The elaborated statement closures of the proved theorems (5,599 and 5,521 constants) are identical to those of the reference challenge statements up to alpha-renaming of hygienic binder names; a mutated reference is detected. A second statement-fidelity reading, written blind to an earlier audit (H9), finds the Lean (C) faithful to Fefferman's (C) and the Lean (D) faithful to (D) as corrected by the Clay errata, with a caveat: the errata's periodic-pressure condition makes the Lean nonexistence claim weaker than a main-text-only reading. It agrees with H9 on every row. A demonstrated limitation. A planted forged declaration (False 'proved' by True.intro, added without kernel checking via debug.skipKernelTC) passes #print axioms with 'does not depend on any axioms'; axiom printing alone is therefore insufficient. A kernel replay rejects it, and the whole corpus passes that replay: 88,400 stored declarations (53,752 Navier–Stokes, 34,648 Euler) were sent to the Lean kernel, REPLAY OK for both; Lean.Replay skips by design the 51 compiler-generated _unsafe_rec auxiliaries (12 NS, 39 Euler; none in any proof closure) and 4 identical congr_simp duplicates. The toolchain's leanchecker on 8 root and statement modules is per-module and not transitive; closure coverage rests on the replay. The paper explains the mechanism step by step. Independent AI audit. A separate AI agent reproduced the replay with its own driver (rc 0 on both closures, forged control rejected), its own #print axioms, kernel-checked identity of the verbatim challenge statements with the solution (four mutants fail), an environment scan, fidelity spot checks, a bit-identical rebuild of 7 modules, mechanised non-vacuity of the reference solution classes, and the Clay PDF sha256. No human has reviewed the audit. What is not established. leanchecker --fresh (Mathlib re-check) was not run; Comparator, lean4export and nanoda were not run (our replay and leanchecker are two drivers of the same Lean kernel, not independent kernels); Mathlib was reused and is trusted, not re-checked; the diff of the challenge file against formal-conjectures@8bf45ed is open; the mathematics of the proof was not refereed by people, and the authors' natural-language papers were not read; the Lean kernel and toolchain are trusted; statement fidelity is a human judgement, made here by AI agents, and no person has audited any statement. If the Lean statement is a faithful formalization of Fefferman's alternative (C) and Lean and Mathlib are sound, the formal object proves alternative (C); that conditional statement is not a Clay determination. Disclosure. The rebuild, the audit scripts and this paper were produced by AI agents (Claude) of one pipeline under the author's direction; the paper stage re-ran no check and uses saved logs. Every claim is tagged A/L/C/X with a claim ledger; the Elenchus ledger gate exits 1 with 0 blocking findings and 4 flags (LEDGER_UNAUDITED_TIER_A, one per Tier A row; open).