Show HN: Formally Verified a Millennium Prize Problem in Coq Yang-Mills Mass Gap

2 points

3 months ago

Hi HN, I'm an independent researcher. Over the last several months, I worked alongside a neuro-symbolic AI daemon to formally verify the Clay Millennium Prize "Yang-Mills Mass Gap" problem directly in the Coq theorem prover.

We mapped the finite lattice topology entirely to the ℝ⁴ continuum by reconstructing the 5 Osterwalder-Schrader axioms, isolating the Millennium formulation into exactly 657 sequential Qed proofs.

We aggressively removed every single heuristic Admitted gap from the main topology. The entire framework now rests on exactly 4 standard textbook axioms (e.g., finite-dimensional Perron-Frobenius theorem, standard statistical mechanics).

The repository contains the raw coqc logic. The formally timestamped preprint is on Zenodo (DOI: 10.5281/zenodo.18726858).

I decided to open-source the kernel execution rather than fight arXiv gatekeepers. Happy to answer any questions about theorem proving, the physics, or the AI methodology.