Gross committee outlines review of OpenAI’s claimed proof that Yang-Mills theory exists: check the definitions in the machine-checkable version, release it, then publish an assessment and the 1147-page proof

Gross committee outlines review of OpenAI’s claimed proof that Yang-Mills theory exists: check the definitions in the machine-checkable version, release it, then publish an assessment and the 1147-page proof

A committee of five scientists chaired by physicist David Gross published a statement on the Kavli Institute for Theoretical Physics website on 28 October, GMT. OpenAI is providing the committee with a version of the proof written in Lean, a language in which software checks each step.

Quantum Yang-Mills theory underpins the description of the strong interaction, which binds quarks into protons and neutrons. Physicists have used it for half a century. In a 2004 report for the Clay Mathematics Institute, Michael Douglas wrote: “At present, there is no satisfactory mathematical definition of quantum Yang-Mills theory.” The institute made this one of its seven Millennium Prize Problems. Arthur Jaffe and Edward Witten formulated the problem as proving that the theory exists and has a mass gap (the smallest nonzero energy of an excitation of the vacuum). OpenAI claims that its model proved the existence of the theory in four dimensions, including quantum chromodynamics, the theory that includes quarks.

On 16 October, after completing the Lean version, OpenAI asked Gross to take custody of the proof and decide how to release it. Gross selected the other four members: Douglas, Jaffe, Igor Klebanov and Nikita Nekrasov. The committee says it acts on behalf of the academic community, is not accountable to OpenAI, and sees incorrect results and failures to credit authors among the risks.

According to the committee’s statement, OpenAI’s work draws on methods developed over decades. The first is Kenneth Wilson’s lattice approach (1974): continuous spacetime is replaced with a grid of points on which the theory can be computed. As the Clay problem description explains, this approach requires proof that the calculations converge to a limit as the lattice spacing approaches zero and its size approaches infinity. Another method repeatedly coarsens the lattice, averaging over fine details; Tadeusz Balaban published a rigorous treatment in the 1980s. The committee writes that Balaban’s ideas are among the key elements that enabled OpenAI to extend the theory to arbitrarily large distances and prove the existence of a limit in which the lattice disappears. The forces in the theory grow with distance. This is thought to imply that quarks remain confined within particles and that a mass gap exists, but the committee describes both questions as open.

The committee will first check that the definitions and problem formulation in the Lean version match those accepted in physics and mathematics, and that this version agrees with the written proof. Lean verifies that a conclusion follows from the definitions as written; people must check whether those definitions capture the intended physical meaning. For example, Anders Hansen of the University of Cambridge and his coauthors argue in a preprint that the Lean version of another OpenAI proof, concerning the Navier-Stokes equations for fluid flow, in places proves a weaker statement than the written account claims.

The committee will then release the Lean version and examine the proof with colleagues. The 1147-page proof itself will be published alongside the committee’s assessment: “Before releasing it, we would like to be sure that it is correct.” On 26 October, when OpenAI announced that the committee was withholding the proof for the time being, the Advisory Group on Mathematics and AI, whose members include Witten, called for the immediate release of both the proof and its Lean version.

The statement concludes: “This is an experiment in how the academic community can respond to the rapid development of new knowledge generated by AI.”