Navier–Stokes in Lean 4: machine-checked analytic core; Clay M6 statement open (NS_M6_OPEN); honest proved-vs-open ledger
-
Updated
Oct 14, 2026 - Lean
Navier–Stokes in Lean 4: machine-checked analytic core; Clay M6 statement open (NS_M6_OPEN); honest proved-vs-open ledger
Lean 4 unconditional proof: riemann_hypothesis_unconditional (B158). 0 sorry, 0 axiom beyond classical trio. 18 minimum sub-atoms proved. Opera Numerorum -- David Fox. DOI: 10.5281/zenodo.20981649
Bost-Connes spectral analysis for X0(143): Gate M1 BC6 Weil bound closed via C(S4)=11.422>2√13 — 16 bricks 0 sorry — Lean 4 — Four Routes condensed into riemann-hypothesis-four-routes 7ce83ae
To associate your repository with the opera-numerorum topic, visit your repo's landing page and select "manage topics."