Physicists Verify OpenAI's AI-Generated Yang-Mills Proof

The Yang-Mills problem has two parts:

• Part one, existence: prove the theory underpinning the Standard Model can be constructed through valid mathematical steps.
• Part two, the mass gap: show that an essential physical quantity called a "mass gap" emerges from the Yang-Mills equations. This part is quantitative and far more difficult—and remains unresolved.

In late October, OpenAI announced its model had solved the first part. The claim cut ahead of another mathematician's public, ongoing collaboration with an employee of OpenAI's rival Anthropic to prove the same result.

Why did OpenAI appoint 'shepherds'?

Like many AI proofs, this one is messy—too lengthy and complicated for human minds to immediately grasp. Seeking to avoid another "slop drop"—the term for when OpenAI unleashed a flood of more than 700 AI-generated proofs on a single day in October—the company enlisted Gross, an eminent American theoretical physicist, to lead a committee supervising the proof's release.

On the night of November 10, Gross and the four colleagues he selected posted a document explaining how the proof works, alongside their affirmation of its formal verification in Lean, a programming language that checks mathematical work.

"We update the progress of our committee in shepherding the LLM [large language model] produced result," the group said in its November 9 statement.

What are the limits of the verification?

The shepherds' document is too cursory to provide a deep understanding of how the proof works. Gross and his colleagues have admitted they still lack that understanding themselves.

"We used OpenAI's Astra [model] to assist with the digestion of the supplied Lean code," they wrote in their assessment. "We do not claim to fully understand the proof yet."

That caveat matters. An affirmation of formal verification in Lean is a machine-checked guarantee, not a human-narrated explanation. With the proof and its Lean code now released, experts can use their own AI agents to reverse-engineer and parse it.

Why are some mathematicians unhappy?

The shepherding approach contradicts recommendations for transparency from an OpenAI-affiliated advisory group and has riled some mathematicians, who see it as needless gatekeeping.

"I'm happy the shepherds are releasing the Lean proof, finally, so we can see what the result is. And I hope, in the future, the AI labs will share their results widely with the community," says Scott Armstrong, a mathematician at New York University. "This review can be done more efficiently and quickly in the open."

The tension is straightforward: gatekept review slows scrutiny; open release accelerates it.

The mass gap problem—part two—remains open, and the community now holds the Lean code it needs to start work.