The committee reviewing OpenAI’s quantum Yang–Mills result made the Lean proof files and its own validation assessment public on November 10. In its November 9 update, the group chaired by physicist David Gross said the submission proves the existence of pure Yang–Mills theory according to standard formulations. The public artifacts let other researchers inspect how the group reached that conclusion.
Track two questions in the Clay problem
The first question is whether a mathematically rigorous quantum Yang–Mills theory can be constructed in four dimensions. That is the part the committee’s assessment addresses. The second asks whether its energy spectrum has a positive mass gap. Roughly, that means a strictly positive threshold separates the vacuum from the first possible excitation. The Clay Mathematics Institute’s problem asks for both.
A reader checking later claims can use the same distinction. Start with the theorem statement in the formal repository and see what conditions it concludes. Then consult the assessment for how those conditions map to the mathematical definition. For any claim about the prize problem as a whole, look for a separate argument about the energy spectrum. The public Lean code makes the construction easier to scrutinize, and the committee’s assessment explains how to read its scope.




