On November 10, 2026, a panel chaired by David Gross, who shared the 2004 Nobel Prize in Physics, published its verdict on an AI-produced proof that OpenAI submitted on October 28. In its judgment, the proof shows that quantum Yang-Mills theory, which describes the force binding quarks, can be built with full mathematical rigor in four dimensions. That is the first of two parts of a Clay Millennium Prize problem. The second, the mass gap, is not proved, so the $1 million prize is not won.
The panel’s 35-page assessment also says: “We do not claim to fully understand the proof yet.” The proof is written in Lean, a programming language that checks proofs mechanically, and the panel relied on its checks.
The verdict was one of four results in 72 hours where software checked AI’s work. On November 9, Anthropic said AI agents had formalized Fermat’s Last Theorem in 30 hours, making its known proof checkable by computer. On November 10, Google DeepMind said its agents had verified key security properties of the core cryptographic code of Signal, the messaging app. On November 11, Amazon Web Services (AWS) released a cloud emulator whose code, it says, its engineers neither wrote nor reviewed.
The panel backs the existence part of the problem
The pure version checked here covers only gluons, which carry the force between quarks. In 2000, the Clay Mathematics Institute made its rigorous construction one of seven Millennium Prize problems, in a statement by physicists Arthur Jaffe and Edward Witten. Scientific American describes the two parts: prove the theory exists, then prove a “mass gap.” In the panel’s terms, every state except the vacuum must carry at least a fixed, positive amount of energy.
OpenAI announced on October 26 that its models wrote an existence proof in plain mathematical prose on September 9, and that it finished a Lean version on October 16. The same post claimed a proof for quantum chromodynamics (QCD), the fuller theory that includes quarks. It also claimed to refute the Exponential Time Hypothesis in computer science, which we covered at the time. On October 17, we reported another AI physics result: counterexamples to a 1967 fusion conjecture.
Gross agreed to lead a group to “shepherd” the physics work. Scientific American reports that he picked the other four: Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov.
The verdict reads: “In our judgment the submission proves that a relativistic quantum field theory satisfying the Wightman axioms can be constructed as a scaling limit of four-dimensional Wilson lattice gauge theory for any simple compact gauge group.” In plainer terms, the proof puts the theory on a grid of points, a lattice, then makes the grid ever finer. It shows that the limit obeys the Wightman axioms, the standard rules for quantum field theories.
The verdict continues: “It does not prove that the infinite-volume limit is unique or that there is a mass gap.”
How a 9,477-file proof was checked
Lean checks each definition and proof step with a small core program called the kernel. Google researchers used Lean to prove quantum programs correct in a paper submitted on November 6.
The panel’s checks began with a clean rebuild of OpenAI’s 9,470 code modules: about 184 minutes, zero errors. All 9,477 Lean source files matched the submission’s file list.
An inventory of 250,319 declarations, Lean’s word for definitions, lemmas and theorems, found no added axioms (assumptions taken without proof) and no “sorry,” Lean’s placeholder for an unproved step. The verification script shipped with the submission then re-checked the 100,168 declarations behind the 17 principal results with a fresh Lean kernel. The proofs use only Lean’s three standard axioms.
A second tool, Comparator, checks a proof against a fixed copy of the target statement and definitions, so an edited statement cannot pass. OpenAI’s public theorem passed on October 30.
After submitting, OpenAI told the panel that this target “omitted some of the connections to the lattice construction.” The panel wrote a stronger combined target, which passed on November 3, and says its assessment of those connections “rests on that stronger target.”
No kernel can say whether the definitions mean what physicists mean. The panel writes that kernel acceptance “does not settle whether those definitions express the intended natural language problem.” Its human review of them was “extensive (but not exhaustive).”
The panel also records “concerns with the quality of the code.” Only 100,168 of the 250,319 declarations, about 40 percent, feed the main theorems. Some names are “unconventional,” such as Farewell.dead in a file called TicketsChart.lean.
Three more machine-checked results in the same week
Google DeepMind’s AlphaProof Code post of November 10 says researchers used several AI models to turn Signal’s security goals into formal specifications, precise statements a machine can check. This was done “with human experts reviewing every one.” Agents running on Gemini Carbon, a Google AI model, then wrote “over six million lines of Lean” to prove that the code meets them.
The agents flagged “just one percent of the codebase” for a human second look. DeepMind says the work took four weeks, “a task that historically takes expert teams years.”
As a test, the team put two real bugs, fixed long ago, back into an isolated copy of the code. Both times, the system produced a machine-checked proof that the buggy version was insecure. Signal’s chief technology officer, Ehren Kret, said prior formal verification “focused on smaller portions of the code.”
Anthropic’s first formalization of Fermat’s Last Theorem, announced on September 4, took a research version of Claude, its AI model, 11 days and 13 million lines of Lean. Anthropic’s launch post, which we covered on November 10, says 1,000 agents using its new Fable 5.2 model redid the work “in just 30 hours, with minimal human intervention.” Their proof is seven times shorter than the first. A footnote added on November 11 says the agents started from “a list of 60 statements,” a one-sentence sketch of the route and “47 proved lemmas from our earlier formalization.”
AWS Emulator mimics more than 200 AWS cloud services on a developer’s own machine, AWS says. Senior principal engineer Matthew Goldberg writes that “our team hasn’t written or reviewed any of the code.”
Agents write tests from AWS’s public API descriptions, which define how programs call its services, and “verify each one against real AWS before submitting.” No change is merged into the code unless it compiles and passes code review by agents, a security check and a fidelity check. On November 12, the public repository listed 29,684 commits, or saved changes. By its last update that evening it listed 30,681, all signed by automated identities.
Limits and criticism
The Yang-Mills verdict covers existence only. OpenAI’s claims for QCD and for a completion of the Standard Model, the theory of the known elementary particles, have no public files and no verdict. The panel lists its assessment of a second OpenAI submission, dated November 4, as “work in progress.”
Comparator ran in a macOS mode without process isolation, the safeguard that keeps programs apart. The runs therefore did not test whether hostile build code could interfere. No independently written kernel was used.
The process also draws criticism. OpenAI asked Gross to lead the group. The panel used OpenAI’s Astra model to help read the code and calls that its “only connection to OpenAI” besides accepting the submissions.
Scientific American calls the document “too cursory to provide a deep understanding of how the LLM’s proof works” and says the approach contradicts transparency recommendations from an OpenAI-affiliated advisory group. New York University mathematician Scott Armstrong told the magazine: “This review can be done more efficiently and quickly in the open.”
The other results have limits too. Wired, republished by Ars Technica, notes that DeepMind’s work “did not, for example, formally verify the entire Signal mobile app” and had a head start from Signal’s earlier verification work. The AWS Emulator README, the project’s guide, rules out “production workloads.” The agents log missing features in a folder named things-that-do-not-work.
What it means
In the Yang-Mills case, machine checking moved faster than human understanding. Anthropic’s September post recalls that Andrew Wiles’s 1995 proof of Fermat’s Last Theorem ran to 129 pages and “required months of painstaking work to verify.” For the Yang-Mills code, the Lean rebuild took about 184 minutes and Comparator passed two days after the code arrived. Thirteen days after receiving it, the panel still did not claim to fully understand the proof.
Human work has moved to the question being checked. The panel spent the first part of its assessment on whether the Lean statement describes Yang-Mills theory; DeepMind’s experts reviewed every specification. In the Guardian on November 13, a Helsinki logician described a similar step in Claude’s work on Gödel’s notebooks: about 200 of the 663 theorems Claude listed had to be repaired for the Coq proof checker, made more precise or given an extra assumption.
AWS’s Swami Sivasubramanian writes on the blog of Amazon chief technology officer Werner Vogels that the engineer’s job is now to “build the specs, tests, and merge gates that decide when that work is correct.” The remaining risk sits in those same checks: a target can miss a property that matters, as OpenAI’s first Yang-Mills target did.
Still ahead are the panel’s assessment of OpenAI’s November 4 submission, any public QCD material and outside mathematicians’ work on the released Lean code. DeepMind says it is open-sourcing its Signal verification files for community use.
Sources
- Validation of the OpenAI Yang-Mills construction, Yang-Mills group (David J. Gross, chair), GitHub, November 10, 2026
- Working with academic communities to build scientific understanding, OpenAI, October 26, 2026
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Pushmeet Kohli and Swarat Chaudhuri, Google DeepMind, November 10, 2026
- Introducing Claude Fable 5.2 and Claude Mythos 5.2, Anthropic, November 9, 2026 (edited November 11)
- Formalizing Fermat’s Last Theorem, Anthropic, September 4, 2026
- How we built the agents that built AWS Emulator, Matthew Goldberg, Amazon, November 11, 2026
- OpenAI’s ‘shepherds’ affirm blockbuster physics result, Joseph Howlett, Scientific American, November 11, 2026
- Google DeepMind just mathematically verified key parts of Signal, Lily Hay Newman (Wired), Ars Technica, November 11, 2026
Header image: chart by MACCUS, data from the Yang-Mills group (November 10, 2026), Google DeepMind (November 10, 2026), Anthropic (September 4 and November 9, 2026), AWS (November 11, 2026) and GitHub (November 12, 2026)
