PhysicsAtoms and particles

Gross committee validates OpenAI Yang-Mills existence proof

Published 13 Nov 20265 min read

David Gross on stage in front of a slide reading The Future of Physics: What We Don't Know — David Gross speaking in Singapore in 2016. Photo: Sinednov, Wikimedia Commons, CC BY-SA 4.0, resized.

On 10 November 2026, a committee of five physicists chaired by the Nobel laureate David Gross published its judgement that a proof written by OpenAI's AI models does what it set out to do: it constructs pure quantum Yang-Mills theory in four dimensions. The same report says the proof does not show a mass gap, so the Clay Mathematics Institute's Millennium Prize problem stays unsolved.

Yang-Mills theory is the mathematics behind the strong force, which holds protons and neutrons together. The pure version describes only gluons, the carriers of that force, with no quarks. Physicists have calculated with it for decades, yet nobody had proved that it exists as a consistent mathematical object. Proving that it does, and that its lightest particle has a mass greater than zero (the mass gap), is one of the seven Millennium Prize problems, each worth $1 million.

Who checked the proof

OpenAI announced the result on 26 October 2026 and said its models had produced the proof on 9 September 2026. It handed the unpublished material to a group led by Gross, with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. Gross shared the 2004 Nobel Prize in Physics for his work on asymptotic freedom in Yang-Mills theories, and Jaffe wrote the official statement of the prize problem with Edward Witten. OpenAI says the members are unpaid and that their conclusions are their own.

The group checked the version written in Lean, a programming language in which every step of a proof is verified by a small trusted program called the kernel. OpenAI submitted that code on 28 October 2026, and the group released it together with its assessment on 10 November 2026.

The numbers behind the check

9,477 Lean source files. A clean rebuild took about 184 minutes and reported zero errors.
250,319 declarations (definitions and theorems, including generated ones). The main theorems depend on 100,168 of them, about 40%.
17 principal results, checked again by a fresh copy of the kernel.
3 axioms, the standard ones for mathematics in Lean: propext, Classical.choice and Quot.sound.

A separate tool called Comparator confirmed that the code proves a fixed reference statement, not a quietly altered one. The reviewers also criticised the quality of the code: about 60% of the declarations are never used by the main theorems, and files carry names such as Kitchen.lean. They used OpenAI's Astra model to help them read the code.

We do not claim to fully understand the proof yet.

Yang-Mills groupValidation of the OpenAI Yang-Mills construction, 10 November 2026source

How the construction works

The proof starts on a lattice. Space and time are replaced by a four-dimensional grid, and the field lives on the links between neighbouring points. This is Wilson's lattice gauge theory. The hard part is shrinking the grid spacing to zero without the answers becoming infinite. That is possible because of asymptotic freedom: the strength of the interaction, the couplingg, falls towards zero at short distances. The report states the law that the constructed coupling obeys at a small distancer:

g_W(r)^2\ \ln\left(\frac{1}{r}\right)\to\frac{1}{2b_0}\ \text{ as }\ r\to0Here b₀ = 11C/(48π²), where C is the Casimir constant of the gauge group.

So at small distances the squared coupling behaves like 1/(2b₀ ln(1/r)). In the graph, x is the distance r in the construction's own units and y is the squared coupling multiplied by 2b₀. The curve falls to zero slowly: cutting r from 0.1 to 0.01 only halves it, from 0.43 to 0.22. The law holds in the limit of small r.

Squared coupling against distance r, in units of 1/(2b₀)

Open in graph

Asymptotic freedom: the coupling fades as the distance shrinks.Drag to pan, scroll to zoom. x from 0 to 0.5, y from -0.289 to 1.73.

Once the spacing has gone to zero, the size of the grid is sent to infinity, and here the proof is weaker. It shows that some sequence of ever larger volumes settles on a limit, not that every sequence gives the same theory.

What is still open

The report lists what the work leaves undone. The infinite-volume limit is not proved to be unique. The construction offers no evidence either way on the mass gap. The report also notes that the problem statement by Jaffe and Witten does not accept a limit found this way as enough unless further properties are proved. OpenAI's wider claims of 26 October 2026, about quantum chromodynamics with quarks and a unified completion of the Standard Model, are not covered by this assessment.

Not everyone accepts the wording. Peter Woit of Columbia University wrote on 11 November 2026 that calling the result a proof of existence is misleading while the mass gap or comparable properties are missing, and he asked for every document to be released. OpenAI's own plain-language manuscript has not been published, and other mathematicians have started writing readable outlines of the Lean code themselves.

What happens next

The group lists a second OpenAI submission, dated 4 November 2026, as work in progress. It says later releases will bring a full review that credits the earlier research the proof rests on. Scientific American reported on 11 November 2026 that the committee had affirmed the result. The Clay Mathematics Institute still describes the problem as unsolved, and the group says it has no present connection to the institute.

Guided courseParticlesQuarks, leptons, the forces and their carriers, and how they fit together in the Standard Model.