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.

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.