yang_mills_mass_gap

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

Yang-Mills existence and mass gap (Millennium Prize Problem): Prove that quantum Yang-Mills theory on R^4 exists and has a positive mass gap Δ > 0 (no energy level between 0 and Δ in the spectrum of the Hamiltonian). Clay Institute offers $1M.

Why this node was retired

The posted statement is

import Mathlib

-- Yang-Mills existence and mass gap (Millennium Prize Problem)
-- The quantum Yang-Mills Hamiltonian has a positive mass gap
-- Formalized using ℓ²(ℕ, ℂ) as the Hilbert space of states
theorem yang_mills_mass_gap :
    ∃ (H : lp (fun _ : ℕ => ℂ) 2 →L[ℂ] lp (fun _ : ℕ => ℂ) 2) (gap : ℝ),
      0 < gap ∧
      ∀ ev : ℝ, 0 < ev → ev < gap →
        ∀ ψ : lp (fun _ : ℕ => ℂ) 2, H ψ = (ev : ℂ) • ψ → ψ = 0 := by
  sorry

The existential Hamiltonian is an arbitrary linear operator with no Yang–Mills or quantum-field structure and may be zero.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

Specify a nontrivial four-dimensional quantum Yang–Mills theory for each compact simple gauge group satisfying explicit field-theoretic axioms, then require vacuum energy 0 and spectrum away from the vacuum contained in [Δ,∞) for some Δ>0. The existence and gap are substantive open content.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.