The mass gap over the compact simple groups — UC Berkeley

A manuscript deriving a mass gap for lattice gauge theory over every compact simple group, constructively over the positive naturals, together with its Lean 4 formalization: two libraries, MassGap and MassGapChecks, Lean core alone, every declaration at the empty axiom set and every check module decided by the kernel. The manuscript is a completed proof of the Yang-Mills mass gap; the Lean tree is its transcription in progress, and the README states which clauses of the main theorem it holds at this version and which remain open.