GI Geometry Intelligence

gi:proof:s437

S437: Lean 4.34.1 port and rebuild of OpenAI's NavierStokesAndEuler formalization (Clay alternatives C and D)

ReleasedBuilder-run · not independently reviewed

Formal statement

Lean declaration names (copyable):

NavierStokes.Comparator.navier_stokes_breakdown_R3
NavierStokes.Comparator.navier_stokes_breakdown_periodic

Verification metrics

Machine-extracted from the repository at pinned commit 3ccc9f72e703.

Lean modules edited21
Kernels checkedLean default, nanoda
Challenge statementsunchanged from upstream

Axiom footprint

Every checked declaration depends only on the three standard Lean/Mathlib axioms:

propext
Classical.choice
Quot.sound

Gates passed

  • Axiom-policy — checked on every build.
  • ECR battery — every result returned as an accepted DECLARATION_CHECK job, zero unused-hypothesis rows.
  • Mutation tests — wrong/weakened statements and inserted sorry are rejected.
  • Non-vacuity — witnesses proved in Lean.

What this is NOT

  • It is not a claimed solution of a Clay Millennium Problem, and has no Clay Institute recognition or independent specialist review.
  • The challenge statements (ComparatorChallenges/NavierStokes.lean) are unchanged from upstream; this is a port and rebuild, not a new result.
  • The mathematics and the Lean formalization are OpenAI’s; this package ports and rebuilds them.

Reproduce it yourself

git clone https://github.com/kts-global/lean-proofs-public cd lean-proofs-public/CLAY_NS_ALTERNATIVES_C_AND_D_FULL_PROJECT_BUILD_S437 # see RECEIPTS/ and PROVENANCE.json; checked on Lean default kernel and nanoda

Expected: axioms: propext, Classical.choice, Quot.sound only

Tested platform: Linux x86_64 only. See the repository’s rebuild docs for online and offline profiles.

Provenance & credit

The blow-up mathematics and the Lean formalization are OpenAI’s (NavierStokesAndEuler @ f9e8bc5b38b6, Apache-2.0). The KTS Global statement and bridge layer, per-alternative packaging, and verification tooling are credited to Tim Jacobs, KTS Global.

Toolchain
Lean 4.34.1 · Mathlib d13f23b
Repository
kts-global/lean-proofs-public @ 3ccc9f72e703
Release
s437-v1

Cite

DOI
10.5281/zenodo.23448690
Wikidata
Q141761720
ORCID
0009-0008-7130-1448

BibTeX & CITATION.cff on the Cite page →

Links