Pinned Loading

1. hodge-abelian-boundaries hodge-abelian-boundaries Public

   First Lean formalization of 200 measured Hodge (2,2)-class obstructions on CM abelian varieties. Clay Wall 3. Applied science: numerical ranks > bounds for g=3,4,5. 0 axiom. 0 sorry.

   Lean 1

2. navier-stokes navier-stokes Public

   Unconditional proof of Navier-Stokes global regularity and mass gap for SU(3). Path A: ESS Backward Uniqueness — COMPLETE. Lean 4. 664 lemmas. 0 sorry. 0 axiom. 0 gaps.

   Lean 1

3. yang-mills-gap yang-mills-gap Public

   Unconditional proof of SU(3) lattice YM mass gap at β₀=ln 8 — Bessel N=5 w1<1/7 + Gross-Witten identity closed → ρ<1/7 → Δ>0. Lean 4.12 664 lemmas 0 sorry trio only 0 OPEN 0 gaps.

   Lean 1

4. p-vs-np p-vs-np Public

   IF SAT ∉ P THEN P ≠ NP — Certified. 223 bricks. 3 barriers. 1 hypothesis. DOI: 10.5281/zenodo.21303093

   Lean 1