OpenAI's Yang–Mills proof: what the Gross committee's assessment confirms and what stays open

On 10 November 2026, the Yang–Mills group chaired by David Gross published the Lean code OpenAI submitted to it on 28 October, together with a 35-page assessment titled "Validation of the OpenAI Yang–Mills construction".¹ Its opening judgment has two sentences. The first says what the group believes is proved: "that a relativistic quantum field theory satisfying the Wightman axioms can be constructed as a scaling limit of four-dimensional Wilson lattice gauge theory for any simple compact gauge group." The second says what is not: "It does not prove that the infinite-volume limit is unique or that there is a mass gap."

So the Millennium Prize problem is not solved, and the assessment does not say it is. The same document says "We do not claim to fully understand the proof yet", and that it rests on the Lean sources alone, not on OpenAI's separate informal manuscript.

Below: what was released, what the group says is proved and not proved, how the Lean code was checked, and the limits the group puts on its own review. Our 31 October explainer covered the committee's first statement, and our 27 October explainer covered OpenAI's announcement. Every source was checked on 11 November 2026. The assessment is the group's own; no journal has reviewed it.

What did the Yang–Mills group release on 10 November?#

Two public GitHub repositories, announced a day ahead in the committee's third statement.⁵ The second statement, on 3 November, had said of the check: "This effort is proceeding well."⁶

• yang-mills-group/OpenAI-YM-20261028³ holds the Lean sources as OpenAI submitted them on 28 October. Its README is OpenAI's own description of the theorem and of how to rebuild it.
• yang-mills-group/YM² holds the assessment, a byte-for-byte copy of the submission, the group's own Lean checks, the dated build and verification records, and instructions for rerunning them.

The third statement describes the assessment as a document "which summarizes the results and our checks of this submission, specifically that it proves the existence of pure Yang-Mills theory according to the problem statements which are standard in physics and mathematics." It thanks Ron Nissim and Fred Rajasekaran, who joined the group on 2 November.¹⁰

The release covers the Lean code only. The committee's first statement had said the proofs produced by the model ran to 1,147 pages and would be released with the group's assessment "When we are satisfied with the quality and correctness of the proofs".⁷ That informal manuscript is not in either repository, and the assessment says of itself: "It does not draw on the separate informal proof manuscript."

The YM repository lists a second OpenAI submission, dated 4 November, as "work in progress".²

What does the assessment say OpenAI's submission proves?#

The construction starts from Wilson's lattice gauge theory, the standard way to put Yang–Mills theory on a grid. The assessment describes three steps.¹

The group then asks whether the object built this way is Yang–Mills theory and not something else. It points to "Its lattice origin, local fields, normalized stress tensor, leading short-distance laws and operator product expansion", which it says "provide substantial evidence that the construction describes Yang–Mills theory." One of those results is a two-point function for the trace of the stress tensor whose leading short-distance coefficient "agrees with the perturbative prediction".

The assessment compares the result with four features that, in its reading, the Clay problem statement by Jaffe and Witten¹¹ requires of a constructed theory.¹

What does the assessment say is not proved?#

The opening page lists three gaps: "no mass gap is claimed. Uniqueness across volume subsequences and agreement of the component theories are also unresolved."¹

The second and third matter because of step 2. A different subsequence of volumes could, as far as the proof shows, give a different limit, and the component theories inside one limit are not shown to be the same theory. The group writes that Jaffe and Witten's formulation "regards a subsequential limit obtained via compactness as insufficient, unless additional arguments establish the requisite properties of the limit", and that the reconstruction and local-field theorems "supply substantial information beyond compactness". It also states its own standard: "Under the existence criterion adopted here, we are not requiring a precise characterization of the vacuum state." And it adds that the missing uniqueness "is not inconsistent with the general expectation that the infinite-volume limit and the true Yang–Mills vacuum are unique."

Section 8 of the assessment lists what the work does not address:

• convergence, not only convergent subsequences, and uniqueness of the infinite-volume limit;
• a probability measure for the continuum theory;
• "a uniform mass gap";
• Wilson loop observables and the area law, which is how confinement is usually stated;
• single-particle states and their energy-momentum spectrum.

Two more limits appear in the body: "Perturbative agreement to all orders remains unproved", and the theorem that rules out free-field descriptions "does not rule out every description in terms of composites of Gaussian fields."

OpenAI's own README draws the same line: "A positive mass gap, general exclusion of continuous-mass generalized free fields and all-orders MS-bar matching are outside its scope."³

How was the Lean proof checked?#

The assessment separates two questions.¹ Verification asks whether the proof follows from its definitions and permitted axioms; Lean's kernel answers that mechanically. Validation asks whether those definitions say what physicists and mathematicians mean by Yang–Mills theory; no kernel can answer that.

The rebuild. A clean build with Lean 4.32.0 rebuilt 9,470 project modules in about 184 minutes with zero errors. All 9,477 Lean source files matched the submission's manifest. An inventory of 250,319 project declarations found no added axioms and no use of Lean's placeholder axiom in the solution. The principal proofs use only the three standard axioms propext, Classical.choice and Quot.sound.

Comparator. Lean lets an author define the objects a theorem is about, so a proof can pass while quietly proving something else. The assessment puts it this way: "A submitted development can, in the process of verification, change the problem statement or one of its underlying definitions and get an invalid proof to appear to verify." Comparator is a tool that checks a solution against a separately fixed reference statement. It passed on 30 October for OpenAI's public theorem, on 3 November for the group's own combined theorem and on 5 November for a separate statement about the operator product expansion. Four controls behaved as expected: a valid proof was accepted, and a changed statement, a forbidden axiom and a changed definition were each rejected.

The group's own Lean checks. The group wrote independent adapters, labelled A1 to A8, proving that the constructed objects meet requirements stated elsewhere. Two compare the submission with formalizations made outside it: the Osterwalder–Schrader axioms of an earlier project, which the group says were formulated "independently and before we learned of the OpenAI Yang–Mills construction", and a finite Wilson lattice law from a separate lattice gauge theory repository. The scope document in the repository is precise about what each covers. The Osterwalder–Schrader bridge, for example, "concerns that scalar family, not a separately specified all-field OS interface", and the analytic estimates it uses come from OpenAI's proof.⁴

Human review. The group reports "extensive (but not exhaustive) human review of the Lean definitions".

One finding concerns OpenAI's own headline theorem. The assessment says that after the submission, OpenAI told the group that its public Comparator target, YangMills.jointExistence, "omitted some of the connections to the lattice construction established by its proof." The group's combined target keeps those connections, and its assessment "therefore rests on that stronger target and the checks described below, rather than on the public existence statement alone."

What limits does the group put on its own review?#

The assessment is open about them.¹

• Understanding. "We used OpenAI's Astra to assist with the digestion of the supplied Lean code. We do not claim to fully understand the proof yet."
• Source. Only the Lean code was assessed. The informal manuscript was not used.
• Attribution. "The OpenAI work rests on prior work by many physicists and mathematicians. A full review with careful attribution will be provided in later releases".
• Isolation. The Comparator runs were made on macOS with a development launcher, so they "do not test isolation of potentially hostile build code." The assessment adds: "An additional external kernel implementation was not used."
• Code quality. The group expresses "some concerns with the quality of the code in the Lean repository." Of 250,319 declarations, 100,168 are used by the main theorems, and it notes "unconventional naming for its declarations and files", with examples such as Cake and cookie in a file named Kitchen.lean.
• Independence. "Our group's only connection to OpenAI (besides accepting their submissions) is the use of their Astra model to help with analysis. Our group has no present connection to the Clay Mathematics Institute."

The repository's submission policy carries a line that applies to this release as much as to future ones: "Posting a submission does not constitute endorsement or certification of its claims."² The group's rules say its assessment will include "our judgment as to whether the proof is correct", and that the group does "not seek academic credit for the discoveries produced by AI models."⁸

Is the Yang–Mills Millennium Prize problem solved?#

No. The problem asks for existence and a mass gap, and the assessment says the construction "does not certify the full Jaffe–Witten problem".¹ The group also says it has no present connection to the Clay Mathematics Institute, which awards the prize. On Papex, Yang–Mills existence and mass gap stays listed as open, with OpenAI's work as a partial claim.

Some early coverage summed the release up as the proof being validated. A more exact summary has four parts:

1. A group of five senior physicists and mathematicians, with two added members, judges that the Lean submission proves existence of a Yang–Mills quantum field theory under a stated existence criterion.
2. The Lean kernel, Comparator and the group's own adapters passed, and anyone can rerun them from the repository.
3. Uniqueness of the infinite-volume limit, the mass gap, confinement and all-orders perturbative agreement are not proved.
4. The group does not yet claim to fully understand the proof, and the informal manuscript is still unreleased.

What happened between the first statement and the release?#

What happens next?#

The group has said what it still owes: a full review "with careful attribution", an assessment of the 4 November submission, and its reading of the informal proofs. The scope document says the November submission's "additional perturbative matching claims" are outside this first package.⁴ The repository invites proposals for further submissions, including on QCD and on a chiral SU(5) gauge theory, without promising to post or review them.²

For other readers, the release changes what can be done. The Lean code is public, so the rebuild and the Comparator runs can be repeated, on Linux with process isolation and with a second kernel. The group's reference statements are public too, so specialists can read the definitions and say whether they agree that these are the right ones. That question, whether the formal statement means what the informal one means, is where the group itself says human review is still needed.⁴

Open questions#

• Does the infinite-volume limit depend on the subsequence, and are the component theories equal?
• Will the informal 1,147-page manuscript be released, and when?
• What does the 4 November submission add, and will the group's second assessment accept its perturbative matching claims?
• Will an independent team rerun the checks with Linux isolation and an external kernel?
• Will the Clay Mathematics Institute say anything about the existence half of the problem?

Sources#

1. Validation of the OpenAI Yang–Mills construction: Assessment 1 (Yang–Mills group, 10 November 2026, 35 pages), checked 11 November 2026 ↩ a b c d e f g
2. yang-mills-group/YM: README, submissions and verification records (GitHub), checked 11 November 2026 ↩ a b c d
3. yang-mills-group/OpenAI-YM-20261028: OpenAI's Lean submission of 28 October 2026 and its README (GitHub), checked 11 November 2026 ↩ a b
4. What the formal checks cover (yang-mills-group/YM, submissions/openai-20261028/docs/checks.md), checked 11 November 2026 ↩ a b c
5. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 3rd Statement by the Shepherding Committee (9 November 2026), checked 11 November 2026 ↩
6. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 2nd Statement by the Shepherding Committee (3 November 2026), checked 11 November 2026 ↩
7. Proof by OpenAI of the Existence of Quantum Yang-Mills theory: Statement by the shepherding committee (October 2026), checked 11 November 2026 ↩
8. Rules and Procedures of the Yang Mills Group (KITP, undated), checked 11 November 2026 ↩
9. Statement by the Yang-Mills Working Group, with the 3 and 9 November updates (KITP), checked 11 November 2026
10. Members of the Yang–Mills group (yang-mills-group/.github, record updated 8 November 2026), checked 11 November 2026 ↩
11. Jaffe and Witten, Quantum Yang–Mills Theory (Clay Mathematics Institute), checked 11 November 2026 ↩