Independent kernel-level verification of OpenAI's Navier-Stokes Lean proof: all four builds pass

pvaa · reddit · 2026-09-11

Context: OpenAI published a 166-page manuscript on Sep 8, 2026 claiming finite-time blowup for forced 3D Navier-Stokes, with a Lean 4 project previously only self-assessed.
The team ran four full builds across two machines on the same pinned commit, including one compiling all 8370 mathlib modules from source (3h13m); all exited 0 with byte-identical outputs.
Key findings: both exported theorems depend only on propext, Classical.choice and Quot.sound; no sorryAx; the 4 sorries in the tree are all Comparator placeholders outside both proofs' closures.
The comparator verified theorem statements match the challenge, and the full solution environment was replayed through two independent kernels (Lean's own and the Rust-implemented nanoda), both accepting; definitions match Google DeepMind's independent formalisation byte-for-byte modulo 21 wrapper hunks.
The team also read all 166 pages twice, ledgered 79 of 79 statements and re-derived a 58-statement spine across 480 steps: Lemma 4.8's outer profile reproduces, but its closure and cone do not at any plottable lambda — the paper's own asymptotics require lambda ≤ 3e-4.
Explicitly not established: the Lean statement is strictly weaker than Theorem 1.1; a green kernel validates the Lean statement only, not the 166 pages; no position on the priority dispute.

More from Research