A Formal Verification Framework for the Yang–Mills Mass Gap: Consensus Framework, Lean 4 and Lattice QCD

This work presents a formal verification framework for the Yang–Mills Mass Gap problem, integrating the Consensus Framework, Lean 4 formalization, and lattice QCD numerical validation. The methodology was recognized as a Global Finalist in the UN Tourism Artificial Intelligence Challenge (2025). The framework combines formal proof, numerical simulation, and AI-assisted consensus validation, fostering interdisciplinary approaches in mathematical physics. This version includes the first validated formulation of Lemma L3 (Topological Pairing), refined after numerical analysis, which establishes its validity across non-trivial topological sectors, marking a critical step towards transforming Axiom 2 into a theorem.