GI Geometry Intelligence

gi:proof:r2r3

Navier–Stokes R2/R3 community verification package, V1

ReleasedBuilder-run · not independently reviewed

Formal statement

Lean declaration names (copyable):

ClayFefferman
ClayFeffermanViaD
NavierStokesComplete
ClayC
ClayD

Verification metrics

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

Theorems in closure40,986
Closure modules620
Comparator exit 0ClayFefferman, ClayFeffermanViaD, NavierStokesComplete, ClayC, ClayD
Verificationpublisher-executed, native Ubuntu 24.04 x86_64
Wall seconds5,678

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

  • No claim about alternatives A or B; they remain open.
  • No claim that the Lean encoding matches Fefferman’s published prose; this has not been independently reviewed.
  • No Clay acceptance, original discovery of the underlying mathematics, or independent replication. Verification runs are publisher-executed on one platform (Ubuntu 24.04 x86_64).

Reproduce it yourself

git clone https://github.com/kts-global/lean-proofs-public cd lean-proofs-public/R2_FINAL_S524_COMMUNITY_V1 ./VERIFY.sh # Ubuntu 24.04; see RESTORE_AND_VERIFY.md

Expected: ClayFefferman, ClayFeffermanViaD, NavierStokesComplete, ClayC, ClayD → exit 0

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
r2-r3-v1

Cite

DOI
10.5281/zenodo.23535805
Wikidata
Q141803373
ORCID
0009-0008-7130-1448

BibTeX & CITATION.cff on the Cite page →

Links