An AI wrote a proof. Now humans have to understand it

A proof handed over, and a door that stays shut

A 1,147-page proof, written by an AI, is waiting for humans to understand it. On October 16, OpenAI asked David Gross, 2004 Nobel laureate in physics, to take custody of it and decide how best to release it to the world. He picked four colleagues to help.

Ten days later, on October 26, OpenAI announced the result. The next day the five physicists put out a two-page statement hosted by Gross's institute in Santa Barbara. One line sums up their position: before they release the proof, they want to be convinced it is correct.

Usually in this story, the company announces too fast and the researchers ask to see the work. This time the text is in the researchers' hands. They're the ones keeping the vault closed.

What OpenAI says it proved

The announcement is broader than most coverage suggests. OpenAI says it has a mathematically rigorous existence proof of certain interacting quantum field theories in four dimensions. Among them: quantum chromodynamics (QCD), the theory of the strong force that glues quarks together inside protons. And the simplest grand unified theory that includes the particles of the Standard Model.

To see why that's a big claim: physics has used these theories for fifty years, with spectacular success, without anyone proving they exist in the mathematician's sense. It's like living in a house for decades without ever having seen the foundations.

Along the way, OpenAI says, it also proves that pure Yang-Mills theory, the version without quarks, exists. That's the piece that made headlines, because it touches one of the Clay Institute's seven Millennium Prize problems, worth $1 million each. OpenAI itself says pure Yang-Mills "is part of" the problem.

The official statement, written by Arthur Jaffe and Edward Witten, asks for two things at once, for any gauge group of a certain type: that the theory exists, and that it has a "mass gap," meaning its particles can't have a mass arbitrarily close to zero. OpenAI claims nothing about the mass gap, and its announcement doesn't say which gauge groups its pure Yang-Mills proof covers. The five physicists list the mass gap among the challenges still open. The prize isn't in play.

Lean checks the proof, not the question

One argument seems to make all this caution pointless. OpenAI says it waited to publish until the proof had been formalized in Lean, a language in which a computer checks every step of an argument. By its own account, it finished that work on October 16, the same day it approached Gross, and nobody outside the company has been able to check it. If a machine has already gone through everything, why wait?

The answer is in the five physicists' statement. Their first job isn't to read the proof line by line. It's to check that the definitions and the problem statement translated into Lean match the ones that are standard in physics and mathematics, and that the formalization aligns with the written proof.

Lean guarantees you proved what you told it to prove. It says nothing about whether you asked the right thing. A flawless spell-checker won't flag a letter addressed to the wrong person. We made the same point here about Navier-Stokes: Lean only checks the statement you hand it.

When even defining a four-dimensional quantum theory cleanly is an open problem, translating the statement is anything but a formality. Once the comparison is done, the five say they will release the Lean proof and, when they're satisfied, the 1,147 pages with their assessment.

Guardians who owe OpenAI nothing

Who are the five? David Gross, co-winner of the Nobel for asymptotic freedom, a key property of these theories. Arthur Jaffe, co-author of the Clay problem statement. Michael Douglas, who wrote a survey of the problem this year. Igor Klebanov, a specialist in quark confinement. Nikita Nekrasov, winner of the 2023 Dannie Heineman Prize for Mathematical Physics.

You might assume OpenAI hand-picked its own reviewers. That's true for only one of the five. Their statement says OpenAI asked Gross to take custody of the proof, and Gross then chose the rest of the committee. They add that they act on behalf of the academic community and have "no responsibility to OpenAI." And they validate nothing: to them, the proof "appears to be an important step."

OpenAI, for its part, went along. Its three results that day follow three different release strategies, each advised by its own guardians: the math result was published as is, the computer science one went to an outside group but was put online right away, and the physics one was left to the group's decision. As of October 29, OpenAI's public repository contains no file on Yang-Mills.

The mathematicians want everything, now

The public disagreement isn't with OpenAI. It's with the mathematicians. On October 26, the day OpenAI announced that the physics group would hold on to the documents, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), an independent advisory group hosted by the Institute for Advanced Study in Princeton, called on OpenAI to release the written proof and its Lean version without delay. Its nine members include Edward Witten, Timothy Gowers and Martin Hairer. The text is collective.

Its argument comes down to two points: understanding should develop in the open, with the same access for everyone, and since the formalization is finished by OpenAI's own account, there is no scientific reason left to wait. The group says it has "great respect" for the scientists OpenAI asked.

The day before, it had published a broader critique of the practice of a lab designating scholars who see a result ahead of everyone else. A head start for a few, a choice that reflects the company's own networks, and names that end up lending credibility. The same group had already declined to play that role when OpenAI released its 722 math manuscripts. It does add that its recommendations are meant for mathematics, not necessarily for other sciences.

So the two authors of the Clay statement end up on opposite sides: Jaffe on the committee that holds the proof, Witten in the group demanding its release.

Verification is the new bottleneck

Nobody in this dispute claims the proof is wrong. The question is who sees it first, and how long it takes humans to know what it actually demonstrates. By OpenAI's account, the machine produced its Yang-Mills proof on September 9. Digesting the methodology and its meaning, the five warn, will take time.

OpenAI itself acknowledges the cost of its approach: choosing the initial shepherds shapes who gets involved first and creates an "asymmetry of information." The five physicists, for their part, call their effort an experiment in how the academic community can absorb knowledge produced by AI. And they say they'll proceed very carefully.