News · 2026-11-12

Gross committee affirms OpenAI's Yang-Mills existence proof in Lean, but says it does not fully understand it

A committee led by Nobel laureate David Gross released a Lean-formalized proof on the night of November 10, 2026 that four-dimensional quantum Yang-Mills theory exists, a result OpenAI says its internal models produced. Scientific American reported on November 11 that the committee affirmed the formal check but wrote, "We do not claim to fully understand the proof yet." No independent outside review has been published.

Key facts

• Claim: OpenAI's models proved existence of pure 4D Yang-Mills (and, per reports, QCD); the "mass gap" half of the Clay Millennium Prize problem is not claimed, and OpenAI reportedly will not seek the prize.
• Committee: David Gross (chair), Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov, per Startup Fortune and Quantum Research Center.
• Reported size: 1,147 pages; secondary sources only.
• Primary source: Scientific American, November 11, which we read in full. We could not open the committee's own document or the Lean repository.

What "exists" means

Start from the well-defined lattice (grid) version of the theory. Shrink the grid spacing to zero and grow the volume to infinity, and show the limit is a genuine interacting quantum field theory satisfying the standard axioms. That was the long-unfinished programme of mathematician Tadeusz Balaban. Predictions in particle physics do not depend on this result; a correct proof would be a landmark for rigorous mathematics, the first interacting 4D quantum field theory meeting the standard axioms. Our lesson on proof assistants explains how Lean works.

Reported timeline, from secondary sources we could not check against a primary one: natural-language proof September 9, Lean formalization finished October 16, announcement October 26 alongside claims on the Exponential Time Hypothesis and the Kakeya conjecture, committee statement November 9, Lean proof and document posted November 10. The OpenAI URL "new-result-theoretical-physics" is an unrelated February gluon-amplitude result; do not confuse them.

What the verification looked like

OpenAI asked Gross on October 16 to take custody of the proof, and Gross chose the other members. The committee says it works for the academic community, not OpenAI. Its statement, as quoted by Scientific American, says the result "proves the existence of pure Yang-Mills theory according to the problem statements which are standard in physics and mathematics." It affirmed the Lean verification and released the Lean code and a short explanatory document, which the magazine calls too cursory to explain how the proof works.

Two admissions matter. The committee wrote: "We used OpenAI's Astra [model] to assist with the digestion of the supplied Lean code... We do not claim to fully understand the proof yet." So the human check leaned on an OpenAI model, and the committee describes its own grasp as incomplete.

The part a Lean check cannot settle

Lean makes "does the proof check?" mechanical, but a formal check is only as good as the theorem statement and definitions it was given: the axioms, gauge groups and what the Lean files actually prove. Outside explainers put the precise statement first on their watch list, and we have seen no outside audit of it. "The Lean proof checks" and "the right theorem was proved" are separate claims.

A transparency fight

The Advisory Group on Mathematics and AI, nine mathematicians including Timothy Gowers, Martin Hairer and Edward Witten, called on October 26 for immediate release, saying the Lean version was complete and there was no scientific reason to wait (reported by Quantum Research Center; Scientific American calls the group OpenAI-affiliated). The committee said it did not want to release something that might be wrong. Scientific American says some mathematicians see the shepherding as needless gatekeeping. Scott Armstrong of NYU told the magazine: "I'm happy the shepherds are releasing the Lean proof, finally... This review can be done more efficiently and quickly in the open."

The context is a "slop drop": the magazine says OpenAI released more than 700 AI-generated proofs in one day in October, and the committee exists partly to avoid a repeat. See our earlier coverage of OpenAI's ten math claims with Lean proofs.

A parallel effort

Ethan Sussman of Northwestern and Levent Alpoge, who works at Anthropic, have been using Claude in public to finish Balaban's programme. Their AI-written manuscripts cover 3D Yang-Mills and QED; they say the manuscripts are not yet satisfactorily vetted and the 4D case is only outlined. The magazine says they thought they were weeks from 4D when OpenAI announced, and credit for AI finishing human-started programmes is unsettled.

What happens next

Outside experts can now use their own AI agents to reverse-engineer the Lean code. Until a statement audit and independent reading arrive, treat this as a promising claim that has passed a mechanical check, not a settled physics verdict. Our sourcing is one magazine article plus secondary aggregators.

Primary source, verified: read the paper →

Ground Truth. (2026, November 12). Gross committee affirms OpenAI's Yang-Mills existence proof in Lean, but says it does not fully understand it. Ground Truth. https://groundtruth.day/news/openai-yang-mills-proof-committee-affirms-lean-check-but-does-not-yet-understand-it.html

@misc{groundtruth:openai-yang-mills-proof-committee-affirms-lean-check-but-does-not-yet-understand-it,
  title  = {Gross committee affirms OpenAI's Yang-Mills existence proof in Lean, but says it does not fully understand it},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {nov},
  url    = {https://groundtruth.day/news/openai-yang-mills-proof-committee-affirms-lean-check-but-does-not-yet-understand-it.html}
}

Topics: openai · mathematics · physics · lean · formal-verification · yang-mills