Reproduce

Reproduce it yourself

Every package ships online and offline rebuild profiles. Each run performs a token scan, builds the Lean modules, and prints an expected PASS line. Tested platform: Linux x86_64 only.

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

git clone https://github.com/kts-global/lean-proofs-public

Expected: axioms: propext, Classical.choice, Quot.sound only · full commands on the proof page.

Navier–Stokes R2/R3 community verification package, V1

git clone https://github.com/kts-global/lean-proofs-public

Expected: ClayFefferman, ClayFeffermanViaD, NavierStokesComplete, ClayC, ClayD → exit 0 · full commands on the proof page.

Lean 4 - Proof - Navier–Stokes C/D (KTS Global)

git clone https://github.com/kts-global/lean-proofs-navier-stokes-cd

Expected: RESULT: PASS (14 axiom-policy checks) · full commands on the proof page.

Lean 4 - Proof - Tao ShortBound to Global Regularity

git clone https://github.com/kts-global/lean-proofs-tao-shortbound-global-regularity

Expected: RESULT: PASS (58 axiom-policy checks) · full commands on the proof page.

CI is cache-assisted: it downloads the Mathlib proof cache and builds the project against it. The from-source claim rests on the builder’s offline rebuild, documented in each repository’s docs/REBUILD_OFFLINE.md.