Inside OpenAI's Yang-Mills Existence Result
On October 16, OpenAI asked David Gross to take custody of a proof. Gross, who shared the 2004 Nobel Prize in Physics for his work on asymptotic freedom, chose four colleagues to join him: Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. Their two-page statement describes the proof as 1,147 pages long and produced by OpenAI's language model. It also says the committee has "no responsibility to OpenAI" and exists to avoid releasing wrong results or omitting attributions.
What the proof claims
The committee describes the result as a proof of the existence of quantum Yang-Mills theory, including coupling to fermions. Yang-Mills theory with gauge group SU(3) coupled to quarks is the part of the Standard Model called quantum chromodynamics, which describes the strong nuclear force. The statement credits three earlier lines of work: Kenneth Wilson's 1974 lattice regularization, renormalization group methods that coarse-grain the lattice, and Tadeusz Balaban's constructive quantum field theory papers from the 1980s. Balaban's ideas, the committee writes, were among the elements that let OpenAI follow the theory to infinite distances and prove existence of its continuum limit.
The statement also lists what the proof leaves undone. Confinement and the mass gap remain open challenges, in the committee's words.
That limit bears on the Clay Mathematics Institute prize. As phrased by Jaffe and Witten, the problem asks for a proof that, for any compact simple gauge group, a nontrivial quantum Yang-Mills theory exists on four-dimensional space and has a mass gap greater than zero. Jaffe co-wrote that description and sits on the committee. News reports on OpenAI's October 26 announcement say the company claims existence only, and that it presents pure Yang-Mills existence as one part of a larger result covering QCD and a unified theory containing the Standard Model. The statement itself names SU(3) and does not say which gauge groups the proof covers, a point the Clay formulation makes relevant.
The timeline OpenAI reports
According to those reports, OpenAI's models produced a natural-language proof of Yang-Mills existence on September 9 and a QCD proof on September 18. The Lean formalization of the Yang-Mills result was finished on October 16, the same day Gross was approached. The committee statement confirms that OpenAI is providing a Lean formalization, which Lean's proof checker can verify step by step.
Lean confirms that a formal statement follows from its axioms. Whether the formal statement matches the physics is a separate check, and the committee has made it the first task. Its stated order of work is to confirm that the definitions and problem statement correspond to the standard ones in physics and mathematics, and that the formalization aligns with the informal argument. After that validation the committee will release the Lean proof. It then plans to study how the proof can be used in quantum field theory, drawing on outside experts, and to publish its assessment together with the full 1,147 pages once satisfied with their correctness.
An earlier claim and its review
On September 8, OpenAI announced a Navier-Stokes result, also with a Lean formalization, making Yang-Mills its second Millennium Prize claim in two months. Clay's president, Martin Bridson, was reported as saying that evaluation would be unhurried and rigorous, and the institute has not accepted the result. Commentators questioned whether the result addressed the forced equations rather than the unforced equations in Clay's formulation, and a credit dispute with the mathematician Tristan Buckmaster followed.
How to reach the committee
The statement asks for all communication to go to YANGMILLS4d@gmail.com. It points readers to Douglas's review, "The Yang-Mills Millennium problem," in Nature Reviews Physics 8, 86-97 (2026), as background on the state of the field. The Jaffe and Witten problem description is hosted on the Clay Institute's website.
The statement gives no release date for the Lean proof or the full manuscripts, saying only that they will come out in due course.
Author bio
David Borish writes The AI Spectator and is the author of The Tony Hawk Paradox: When Video Games Predict Reality. More at davidborish.com
