Independent verification: openai/NavierStokesAndEuler + fluid_lean — builds green, axiom audits standard-trio

[ajmwagar]

Independent verification: openai/NavierStokesAndEuler + tristanbuckmaster/fluid_lean

Both builds green. All ten audited theorems depend only on [propext, Classical.choice, Quot.sound].

We (Future Present Labs — a machine shop in Seattle, not a formal methods group) independently verified both of this week's fluid-equation formalizations. Raw logs, per-step exit codes, SHA256SUMS manifests, upstream git bundles, and the exact pinned commits are all committed at https://github.com/FuturePresentLabs/ns-verify (this repo). Human-reviewed axiom audits are in audits/.

---

Method

1. Clone upstream at a pinned SHA into detached HEAD, assert clean git status
2. lake build, naming every declared lean_lib (not just defaultTargets — see caveat 3)
3. #print axioms on the headline theorems

Each bundle ran on a fresh 16 vCPU / 128 GiB ephemeral cloud machine, one bundle per invocation, with a SHA256SUMS manifest generated on the verifying box. Reproduce it yourself with make run (docs/RUNBOOK.md).

OpenAI — NavierStokesAndEuler @ 8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538 — toolchain v4.34.0-rc2

• lake exe cache get + lake build: success, 11,251 jobs, exit 0 (41m57s solo)
• Axiom audits, all four clean:

'NavierStokes.Comparator.navier_stokes_breakdown_R3' depends on axioms: [propext, Classical.choice, Quot.sound]
'NavierStokes.Comparator.navier_stokes_breakdown_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Euler.euler_breakdown_R3' depends on axioms: [propext, Classical.choice, Quot.sound]
'Euler.exists_compact_smooth_euler_singularity' depends on axioms: [propext, Classical.choice, Quot.sound]

Buckmaster — fluid_lean @ d0124689230b58b4f86e7b90ac59de06404b3b6b — toolchain v4.32.2

No Mathlib cache exists for this toolchain → from-source builds: euler-blowup 9,776 jobs, exit 0 (4h07m); boussinesq-blowup and affinecore exit 0. All six audits clean, including:

'euler_smooth_force_blowup' depends on axioms: [propext, Classical.choice, Quot.sound]
'boussinesq_smooth_force_blowup' depends on axioms: [propext, Classical.choice, Quot.sound]
'forced_boussinesq_affine_core_blowup' depends on axioms: [propext, Classical.choice, Quot.sound]

(Full list of all ten audited theorems across both repos in audits/.)

Caveats, stated plainly

1. sorryAx appears in no axiom output. Seven declaration uses 'sorry' warnings exist, all in statement-side challenge/comparator files (4 in OpenAI's ComparatorChallenges, 3 in Buckmaster's Challenge.lean), and none is in any audited theorem's dependency closure.
2. The Buckmaster bundle ran in resume mode — it reused .lake artifacts from earlier runs on the same pinned commit after asserting a clean tree at that exact SHA. The from-scratch compiles happened in the earlier bundles, also committed.
3. Reproduction warning for affinecore: its lakefile sets defaultTargets = ["AffineCore"] and omits the comparator libraries, so a bare lake build exits 0 without ever compiling Solution.lean — the file binding forced_boussinesq_affine_core_blowup to its proof. If you reproduce, name all declared libraries explicitly.
4. Usual disclaimer: a clean build means Lean accepted the pinned source under the pinned toolchain. It does not establish that the formal statements faithfully encode the informal claims, and it is not a substitute for mathematical review. One scope gap on our end: OpenAI's optional Comparator replay needs tooling we didn't provision, so we don't claim that step.

Reproducing

Everything is in the repo: make run provisions an equivalent machine, runs the verification, pulls checksummed evidence, and tears the infra back down (docs/RUNBOOK.md).

If you verify either repo at these or later SHAs — or get a different result — please post it in this discussion. Independent confirmation or refutation is the entire point of this thread.

---

Avery Wagar — Future Present Labs LLC. Background: software, lots of CFD/CAD. First time touching Lean; the proof checker did not care.