6th-grade Peano arithmetic broke OpenAI's $100B Yang-Mills mass gap proof

The repository presents a Lean 4 formalization claiming that the canonical constructive Yang-Mills framework on noncompact ℝ⁴ cannot meet both the full Osterwalder-Schrader/Wightman axioms and a strict positive spectral mass gap. It calls this a negative resolution of the existence problem, rather than a construction of a Yang-Mills theory. Its central theorem says the two requirements are incompatible for every model in a specifically defined class, InCompleteR4GaugeClass. A second no-go claim applies to models deemed physically admissible under an explicit assumption that infrared modes cannot disappear without a horizon or boundary cutoff. The project reports a 3,705-line Lean proof with no admitted lemmas or declared axioms.

To support the incompatibility claim, the repository describes several obstruction routes, including gauge-fixing difficulties associated with Gribov-region boundaries, a gauge-independent locality and positivity obstruction attributed to Strocchi, and a Cauchy-Wick obstruction. It argues that any one route can defeat a package defined as a conjunction of axioms, and that dropping one proposed method does not remove the others. The stated scope is limited: it does not construct a positive ℝ⁴ solution, establish the Clay prize, rule out formulations beyond its chosen class, or prove a continuum limit from a separate compact-manifold construction. The Lean kernel can verify the encoded deductions; whether the formal definitions and assumptions capture the intended physical theory is a distinct question readers would need to assess.