---
type: analysis
slug: research-of-three-ai-proof-claims-only-the-qcd-proof-is-unreleased-eth-and-cfsg-await
title: "Of three AI proof claims, only the QCD proof is unreleased; ETH and CFSG await human review"
description: "OpenAI's QCD existence proof is held by a Gross-led committee, the ETH refutations and Axiom's CFSG formalization are public and Lean-checked, and no independent expert has finished verifying any of them."
published_at: 2026-11-09T20:00:00.000Z
topics: ["openai","anthropic","research"]
source_urls: ["https://openai.com/index/building-scientific-understanding-with-academic-communities/","https://www.kitp.ucsb.edu/sites/default/files/YM_working_group.pdf","https://www.science.org/content/article/ai-cracks-27-year-old-pillar-computer-science-openai-and-anthropic-claim","https://raw.githubusercontent.com/anthropics/formal-math/main/eth/README.md","https://blog.computationalcomplexity.org/2026/10/the-exponential-time-refutation.html","https://axiommath.ai/research/the-enormous-theorem-formalized/","https://raw.githubusercontent.com/AxiomMath/CFSG/main/README.md"]
author: "Andrey Reshetnikov"
author_profile: https://newruntime.com/owner-profile.md
---
Within about 48 hours, AI labs announced three extraordinary results: OpenAI (and, separately, Anthropic) claimed a refutation of the Exponential Time Hypothesis, OpenAI claimed rigorous existence proofs for QCD and pure Yang-Mills in four dimensions, and Axiom released what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups, the longest proof in mathematics. Each arrived with a different release model, from immediate public dumps to a committee holding the proof back.

For builders, the question is not whether models can do mathematics but what an announcement actually certifies: whether the artifacts exist publicly, whether a proof checker accepted them, whether the formal statement says what the paper says, and whether any independent human has finished checking.

## What we checked

- **Where are the complete proof artifacts, formal verification records, and independent expert assessments needed to evaluate each claimed result?** partly confirmed. ETH: OpenAI and Anthropic both published papers and Lean projects, with expert shepherds and a review conference planned, but no completed human verification. QCD: the 1147-page proof is withheld by the Gross committee pending its own assessment, with only Yang-Mills existence reported as Lean-formalized. CFSG: Axiom's 43.1M-line Lean repo is public, the errata list is not yet out and no outside rebuild is reported in the sources I opened. [1][2][3][4][5][6]

## What we found

- The quantum chromodynamics claim is the least checkable of the three. OpenAI says its models produced a rigorous existence proof for four-dimensional gauge theories with fermions, including QCD, but on the advice of its physics shepherds it has not released the AI output. The KITP working group led by David Gross says it will publish the proof only with its own assessment and once it is convinced the proof is correct; Science reports the manuscript runs to 1147 pages. [1][2][3]
- Even if correct, the physics result is not a Millennium Prize solution. The shepherds' own statement says confinement and the mass gap, the part of the Clay problem beyond existence, remain open. OpenAI's announcement describes pure Yang-Mills existence only as a subproblem that is part of the Clay problem. [2][1]
- For ETH, OpenAI's artifacts are public: its computer-science shepherds (Impagliazzo, Paturi, Williams) chose to publish the natural-language proof and the Lean formalization immediately on GitHub. Science reports that both OpenAI and Anthropic say Lean verified their results but that no human has yet fully confirmed the proofs, and the ETH group plans a fully human-readable proof and a virtual review conference before year end. [1][3]
- Anthropic's parallel ETH refutation is also fully public, paper and Lean 4 project, but went out with no external reviewers. Its README is explicit that Lean checks the proofs while nothing mechanical checks that the short statement file matches the paper, which is the gap a human reviewer has to close. [4][3]
- Independent expert opinion on ETH is favourable but not a verification. Lance Fortnow writes that ETH is probably toast while saying he has not checked the proof, and notes the shepherds have set up a public discussion site and paper repository. [5]
- The third claim, a complete machine-checked proof of the largest theorem, matches Axiom's Lean formalization of the Classification of Finite Simple Groups (my reading of the truncated story title). Axiom says agent swarms wrote about 43.1 million lines of Lean in 24 days and the repository is public, sorry-free and uses Lean's standard axioms. It also found 34 noteworthy deviations from the published record, with the errata list promised but not yet released, and the build takes up to a day, which raises the bar for outside re-checking. [6][7]

## What it means

Treat these as three different evidence levels. The ETH refutation is the strongest: two labs, public Lean projects checked with standard axioms, and the original proposers of ETH organizing review; build on it cautiously but expect it to hold. CFSG was a known theorem, so the formalization's value is the artifact and the errata; it is public but enormous, so independent rebuilding is the next real check. The QCD claim is currently an announcement plus a shepherds' statement, with nothing anyone outside can inspect.

If you build AI-for-math or verification tooling, the recurring weak point is statement fidelity and human-scale review, not proof checking. Lean acceptance covers the deductions; it does not cover whether a short statement file or a 43-million-line development formalizes the intended theorem. Tools that make statement audit, reproducible builds and artifact provenance cheap are where the bottleneck now sits.

## Competing readings

- **The ETH refutation will survive expert review, while the QCD claim stays unassessable until the committee releases it** (likely, about 65%). What would tell it apart: Two independent Lean-checked ETH refutations are public and expert shepherds are organizing review [1][3]; The QCD proof is withheld until the committee is convinced it is correct [2].
- **A statement-fidelity flaw in the Lean files will weaken at least one ETH claim, showing machine checking overstated certainty** (unlikely, about 25%). What would tell it apart: No machine checks that the statement file matches the paper, and humans have not finished checking [4][3][5].
- **The QCD proof is substantively flawed or narrower than announced once released** (very unlikely, about 10%). What would tell it apart: The mass gap remains open and the proof is a 1147-page manuscript not yet assessed [2][3].

## Base rate

The New Runtime archive holds only 4 earlier research stories about companies, projects or standards from the last 12 months that are at least 3 months old: too few (minimum 5) for a base rate. The archive has only 4 comparable earlier research stories, 2 of which were followed by a release within 90 days. That is below the minimum of 5, too few for a base rate, so this analysis does not lean on it.

## What would change this view

- Shepherds or outside theorists report that an ETH Lean statement does not match the paper's theorem (signal): Machine checking certified the wrong statement and the refutation is in doubt.
- The Gross committee releases the QCD manuscript with a positive assessment and a Lean formalization covering QCD (model-listing signal): The physics claim moves from announcement to checkable result.
- An independent group rebuilds Axiom's CFSG repository and audits the TauCeti statement (open-source signal): The CFSG formalization is independently confirmed rather than self-reported.

## Still open

- When will the Gross committee release the QCD proof and its assessment, and has the QCD part (beyond Yang-Mills) been formalized in Lean?
- Has anyone outside OpenAI and Anthropic confirmed that the ETH Lean statement files faithfully match the papers?
- Will an outside group rebuild Axiom's CFSG development, and what is in the promised errata list?

## Sources

1. [OpenAI: Working with academic communities to build scientific understanding](https://openai.com/index/building-scientific-understanding-with-academic-communities/) (primary)
2. [KITP Yang-Mills working group statement](https://www.kitp.ucsb.edu/sites/default/files/YM_working_group.pdf)
3. [Science: AI cracks a 27-year-old pillar of computer science](https://www.science.org/content/article/ai-cracks-27-year-old-pillar-computer-science-openai-and-anthropic-claim)
4. [Anthropic formal-math eth README](https://raw.githubusercontent.com/anthropics/formal-math/main/eth/README.md)
5. [Computational Complexity blog: The Exponential Time Refutation](https://blog.computationalcomplexity.org/2026/10/the-exponential-time-refutation.html)
6. [Axiom: Formalizing the Enormous Theorem](https://axiommath.ai/research/the-enormous-theorem-formalized/)
7. [AxiomMath CFSG README](https://raw.githubusercontent.com/AxiomMath/CFSG/main/README.md)

Author: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Anthropic](https://newruntime.com/topics/anthropic.md): Explore the anthropic topic hub.
- collection: [Analysis](https://newruntime.com/analysis.json): Open the latest authorial analysis.
- collection: [Sources](https://newruntime.com/sources/): See the original sources this archive cites.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)