Show HN: Zero-axiom Lean 4 proof that Yang-Mills on R^4 is a "round square"

Category: other

Tags: lean4, formal-verification, mathematical-physics, theorem-proving

Score: 4.7/10 (Innovation: 6, Technical: 6, Documentation: 3, Utility: 2)

This project presents a Lean 4 formalization of a claimed negative resolution to the Yang-Mills mass gap problem on non-compact R^4, arguing that demanding both the Osterwalder-Schrader/Wightman axioms and a strict spectral gap leads to a contradiction. It is presented as zero-axiom and open-source, but the extraordinary claim and low community engagement warrant skepticism.

Target audience: mathematicians, theoretical physicists, formal verification researchers

Repository: https://zenodo.org/records/23918639/files/RoundSquare.lean?download=1

View on Hacker News