# Yang-Mills Group Announces Public Review Plan for OpenAI Lean Proof By Simon Yoon Canonical URL: https://www.tokenpost.com/news/technology/53471 Published: 2026-11-11T01:55:35.000Z Updated: 2026-11-11T01:55:35.000Z Section: Technology > The announcement outlined separate GitHub repositories for the formalization and the group’s validation assessment. The Yang-Mills Working Group set Nov. 10 as its target to publish OpenAI’s Lean formalization and a committee assessment of a pure Yang-Mills existence proof tied to a Millennium Prize problem. The plan calls for two GitHub repositories: one containing the Lean code and another containing the group’s validation. Nobel laureate David J. Gross leads the working group. Lean is a proof assistant that lets a computer check deductions in a mathematical argument once its claims and steps are encoded in a formal language. The committee’s assessment is intended to examine whether the proof’s definitions and problem statement match those used in physics and mathematics. That review addresses a limit of computer verification: Lean can check reasoning within an encoded statement, but that check alone does not establish that the statement captures the intended physical problem. OpenAI produced a natural-language existence proof on Sept. 9 and completed the Lean formalization on Oct. 16, when the review group was convened. Questions about the mass gap and confinement remain unresolved. TokenPost previously covered [OpenAI’s broader mathematical and physics work](). ## Links in this article - [OpenAI’s broader mathematical and physics work](https://www.tokenpost.com/news/technology/41756)