News
Product updates, engineering notes, and field evidence from independent software verification.
Latest
The Lean code of the Navier–Stokes/Euler formalization as it was verified: the repository structure, the trust model of a prebuilt-.lake replay, the theorem surface, the torus machinery behind (8.19), the R3 comparison machinery, the Euler side, and the two repair commits.
Read the update →The Lean formalization of OpenAI's Navier–Stokes blowup argument verifies green. The paper's argument does not survive a step-by-step reading: its closing estimate (10.19) rests on three claims that are each false, and the bound itself is false under its own quantitative hypotheses — with a counterexample family whose pressure flux is nonzero while the right-hand side of the estimate is exactly zero.
Read the update →A step-by-step walkthrough of the argument in OpenAI's Navier–Stokes blowup manuscript — the claim, the construction, and the closing argument of §10.3 — with a machine-verdict attached to every step where a machine can decide it.
Read the update →The Lean formalization of the OpenAI Navier–Stokes blowup argument, presented as a mathematical proof: the formal statement, the proof structure, a per-step mapping (math step ↔ Lean lemma ↔ verification status), the (10.19)′ repair as the formalized bridge, and the signed verification report as the evidence layer.
Read the update →