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

On October 26, OpenAI announced a claimed "bare existence" proof in Balaban's RG programme on pure R^4—but notably stopped right before claiming the mass gap Δ > 0. It turns out there is a rigorous mathematical reason why no compute cluster can bridge that gap on flat infinite space.<p>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.<p>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).<p>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`.<p>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.<p>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.<p>You can verify the code in your browser without installing anything: 1. Download the script from the URL above. 2. Go to <a href="https://live.lean-lang.org" rel="nofollow">https://live.lean-lang.org</a> 3. Load the file from disk and check the verdicts.<p>Full preprint with context: <a href="https://doi.org/10.5281/zenodo.21555360" rel="nofollow">https://doi.org/10.5281/zenodo.21555360</a><p>Would love to hear feedback from the logic and constructive math folks here.