Show HN: Zero-axiom Lean 4 proof that Yang-Mills on R^4 is a "round square"
zenodo.org
I wrote a 2,576-line self-contained Lean 4 script (`RoundSquare.lean`) that formally proves a negative-result resolution to the Clay Millennium Yang-Mills problem on pure R^4. In the tradition of Gödel and Turing, it proves that demanding BOTH the full Osterwalder-Schrader/Wightman axioms AND a strict spectral gap Δ > 0 on non-compact R^4 is a structural contradiction.
Bare existence (Δ = 0) satisfies the OS axioms on R^4. But forcing a strict gap (Δ > 0) strictly requires an infrared cutoff via the Gribov horizon and a non-local θ-vacuum projector on the boundary S^3_∞, which immediately destroys Wightman microcausality (Strocchi's theorem) and Wick holomorphicity (GZ complex poles).
The Lean 4 script compiles in 2 seconds with ZERO axioms. No `sorry`, no `Classical.choice`, no `propext`. Every single one of the 74 `#print axioms` checks outputs `does not depend on any axioms`.
While corporate AI labs keep their training data and exact models closed, I believe the future of theoretical physics and millennium-level mathematics must be 100% open-source, machine-verified, and axiom-free.
I've put a 10 LTC bounty on X for anyone who can find a logical flaw in the 74 theorems or exhibit a constructive mechanism on pure non-compact R^4 that generates a strict gap while bypassing the FMR horizon cusps and the S^3_∞ projector.
You can verify the code in your browser without installing anything: 1. Download the script from the URL above. 2. Go to https://live.lean-lang.org 3. Load the file from disk and check the verdicts.
Full preprint with context: https://doi.org/10.5281/zenodo.21555360
Would love to hear feedback from the logic and constructive math folks here.