Yang-Mills Working Group to publish OpenAI’s Lean code for review

A committee of physicists and mathematicians is about to put an AI-generated proof on public display.

The Yang-Mills Working Group, headed by Nobel laureate David J. Gross, said on November 9, 2026, that it plans to publish OpenAI’s Lean code and its validation the following day.

The release concerns one of the most famous open problems in mathematical physics. It’s a Clay Mathematics Institute Millennium Prize problem centered on quantum Yang-Mills theory, the framework underneath quantum chromodynamics, which describes the strong force.

What is being released

The working group intends to publish two GitHub repositories on November 10, 2026.

The first contains OpenAI’s full Lean code submission. The second is a validation assessment, described as confirming the existence of pure Yang-Mills theory according to established definitions in physics and mathematics.

Lean is a proof assistant, a programming environment where a mathematical argument is written so precisely that a computer can verify each step.

The timeline runs back a few months. OpenAI produced a natural-language existence proof for quantum Yang-Mills theory on September 9, 2026.

The Lean formalization was completed by October 16, 2026. That same day, OpenAI made its initial contact with David J. Gross, and the committee was convened to carry out an independent review and validation.

OpenAI did not publish the work immediately. It sent the material to the committee for rigorous review first.

The size of the thing

The Lean proof submitted to the committee totals 1,147 pages.

According to the research summary of the committee’s approach, reviewers focused heavily on whether the definitions and the problem statement in the proof actually match the ones the field uses. In formal mathematics, a proof can be perfectly valid and still prove the wrong thing. If the definitions drift even slightly from the accepted ones, a computer will happily certify an answer to a question nobody asked.

The work is described as building on foundational tools in the field, including Wilson lattice regularization and Balaban’s renormalization-group methods.

What it does not solve

The proof addresses existence. The questions of mass gap and confinement remain unresolved, according to the research findings. Those are the remaining challenges tied to the Millennium Prize problem.

The summary language around the proof also carries a hedge. It was suggested to address the existence of the quantum theory, and the forthcoming validation repository is where outside readers will get to inspect the committee’s reasoning for themselves.

Background: a crowded field

OpenAI is not the only group working on this terrain in public.

Parallel efforts are underway, including a repository from Ethan Sussman and Levent Alpöge that explores approaches from constructive quantum field theory.

The involvement of David J. Gross also lends the process weight. A committee led by a Nobel laureate is a different proposition from a company blog post declaring victory.