A multi-agent AI framework formalizing the Yang-Mills Mass Gap finite-lattice theory in Lean 4 without axioms or sorry.
-
Updated
Sep 7, 2026 - Lean
A multi-agent AI framework formalizing the Yang-Mills Mass Gap finite-lattice theory in Lean 4 without axioms or sorry.
Geometric Exclusion of Smooth Solutions to Navier-Stokes Equations at Stationary Right-Angles under No-Slip Boundary Conditions in Lean 4.
An adversarial, fully-banked search for a Navier-Stokes blow-up certificate: 440 legs, no solution found, and an honest record of why. Every claim tiered, every gate falsifiable, all data banked. Independently kernel-checked the Lean Navier-Stokes formalisation. MIT + CC BY - fork it and carry on.
To associate your repository with the millennium-prize-problem topic, visit your repo's landing page and select "manage topics."