Papex
Explore
← Blog

Explainer15 min read

Has the ETH refutation been verified? What has been checked, and what would confirm it

Four days after OpenAI and Anthropic claimed to refute ETH, the open examination has begun. What has been checked so far is a toy model and the Lean builds, not the theorem.

Papex

On this page
  1. What did the examiners ask OpenAI for?
  2. What does the open examination look like in practice?
  3. What did the community notes in PR #60 check?
  4. Has anyone rechecked the Lean proofs?
  5. What are the first follow-up papers?
  6. What have named researchers said since?
  7. What would count as confirmation?
  8. What changed on Papex?
  9. Sources

Four days after OpenAI and Anthropic each claimed to have refuted the Exponential Time Hypothesis (ETH), no one outside the two companies has published a verdict on either claim. The examination that Russell Impagliazzo, Ramamohan Paturi and Ryan Williams agreed to organize has started in public, with a discussion blog, a shared folder of notes, a feedback form and a proposed virtual meeting before the end of 2026. Volunteers have rebuilt the Lean proofs, written expositions and run small experiments. The first follow-up papers already build on the result.

What has been checked so far is narrower than the activity suggests. The most concrete public test of OpenAI's paper is a set of community notes merged into a volunteer repository on 29 October. It runs the paper's construction on formulas with at most 14 variables and compares every result with brute force. Its author writes that the notes "do not bear on the correctness of the theorem".

On 27 October we put the two claims side by side in OpenAI's Kakeya, ETH and Yang–Mills claims. This post covers what has happened since: what the examiners asked of OpenAI, what the open examination looks like in practice, what has and has not been checked, the first follow-up papers, and what would count as confirmation. Every source was checked on 30 October 2026.

What did the examiners ask OpenAI for?#

Two things: the raw data, and a conference. Williams announced the examination in a four-part thread on X and on Bluesky on the evening of 26 October (UTC). The second post reads: "We've signed no NDAs and will receive no compensation, so we are free to share our ongoing findings with the community, which we intend to do throughout the process. We've asked OpenAI to publicly release ASAP all their raw data regarding ETH, including PDFs and Lean source." The third: "We have also asked OpenAI to commit to sponsoring a conference for the benefit of the entire community affected by this work. They agreed to both."

OpenAI's announcement says the same in its own words: "We have agreed to the group's requests that all raw data of the results be made public to facilitate independent verification by the community, and that OpenAI commit to funding a conference to understand the implications of this work on the field as a whole." Named coverage reported it that way too. Ana Maria Constantin wrote in The Next Web on 26 October: "The group asked OpenAI to release all its raw data on the ETH result and to fund a conference for the research community. OpenAI agreed to both, according to Williams and OpenAI." Scientific American reported the conference "according to Williams" on 27 October.

The examiners did not get privileged access. Asked on Bluesky whether he could put more questions to the model, Williams replied: "We do not have access to their internal models. We only got the PDF, which I have posted here."

What is public now:

  • On GitHub. The ETH folder of openai/math holds the paper, its TeX source and a citation file, and the Lean development sits in the repository's Lean library. The repository's only update since 26 October, dated 29 October, concerns a different result (Hodge, for CM abelian varieties). OpenAI has published abridged reasoning summaries for ten other results; ETH is not one of them.
  • In the organizers' folder. The examiners' shared folder (below) has an OpenAI subfolder with the released paper and a second OpenAI manuscript: 17 pages, titled "Exactly Counting 3-SAT Solutions in Subexponential Time" and dated 17 October. It claims a weaker exponent, with a smaller power of log n, and calls the released paper its "companion manuscript". It is not among the preprints in OpenAI's GitHub repository.

The sources we read do not spell out what "all raw data" will include.

What does the open examination look like in practice?#

It looks like a small research community organizing itself, mostly through shared files. The organizers' opening post on ethdiscussion.blog, signed by all three, repeats their letter: "Our involvement should not be taken as certification of the claim." It defines the job: "The immediate task is to examine the argument, establish its correctness or identify its limitations, and understand its consequences." It asks for ideas on how researchers can "contribute independently while sharing questions, gaps, corrections, and verified steps".

It lists four arrangements:

  • The release URL, "the authoritative location for the original PDFs, any accompanying source or formalization, and subsequent corrections".
  • ETH_Repository, a view-only Google Drive folder kept by the three organizers "to facilitate dissemination of researchers' notes, explanations, comments, corrections, and follow-up results". Its ReadMe says contributors email Paturi and get a folder under their own name.
  • A Google Form asking for feedback and about "the desirability, format, and timing of a proposed virtual meeting before the end of 2026".
  • The blog itself, for news and public comments. The ReadMe also points to a Zulip chat set up by Holger Dell.

On 29 October the blog published a second post, "Links To Other Work", by Francis Zane, pointing to expositions by Mark Sellke, Ryan O'Donnell and Shiva Kintali and to Lance Fortnow's blog. On 30 October the shared folder held:

KindWhat the folders hold
The claimsOpenAI: the released paper and the 17-page manuscript. Anthropic: its paper
The organizersA five-page note by Impagliazzo and Paturi, dated 28 October, on a weaker form of ETH
ExpositionsRyan O'Donnell: 13 numbered drafts of his exposition from 26 to 29 October, other notes and a lecture link. Mark Sellke: slides. Shiva Kintali: a simplified proof. Eitan Porat: slides and a video. Jesper Nederlof: a "Claude ETH refutation working note" on Anthropic's paper, marked "work in progress". Amit Sahai's folder: "An Elementary Route to Subexponential 3-SAT"
Further workIsaac Rudich: a factoring paper built on the counting algorithm. Tony Newton: a note on structures in OpenAI's construction, which says it claims no "independent refutation of ETH"

The organizers' own note proves that a weaker form of the hypothesis, Weak ETH, holds for 3-SAT exactly when it holds for k-SAT. It does not assess either claim. We found no findings from the examiners on the claims themselves, on the blog, in the shared folder or in Williams' posts on X and Bluesky, as of 30 October.

What did the community notes in PR #60 check?#

They check a toy model of the algorithm, not the theorem. The notes sit in oai-math-revised, a volunteer repository that collects corrections, references and reading groups for OpenAI's manuscripts. Its README says the effort "is entirely independent and is neither sanctioned nor sponsored by OpenAI". Chelsea A. McElveen opened pull request #60 on 28 October, and Soledad Villar merged it on 29 October. It adds three files to the ETH paper's folder: NOTES.md, a Python script and a short README for the script.

The script, in the PR's words, is "an executable model of Sections 2.3–2.7 checked against brute force at n ≤ 14". It builds the paper's polynomials, its "measurement designs" and its interpolation step for small formulas, uses exact arithmetic, and compares each stage with a count of all 2^n assignments. With a simple "direct" design, which the notes say "compresses nothing", the reconstructed count matches brute force on formulas with 10, 12 and 14 variables: 259, 736 and 3,108 satisfying assignments. With the paper's own Section 2.7 construction at its smallest parameters (r = 2, Q = 2, R = 2), the whole pipeline runs on a 6-variable formula and gets the right count, 34, and the key identity checks out on a 12-variable formula.

The notes add two structural remarks on Section 2.7. One describes how variables cluster into groups as the formula grows; the other works out that this "does not change the exponent", and the notes call it "structural, not algorithmic". They also make two suggestions for clearer exposition. The PR is explicit about its limits: "Does not change the TeX source or the manuscript's claims. No error in the manuscript is asserted." The notes themselves say: "These notes do not bear on the correctness of the theorem, whose formal verification is the Lean development".

Why a toy cannot settle it. ETH is a statement about how running time grows as the number of variables goes to infinity. At 14 variables, brute force checks 16,384 assignments. A small run can show that each step computes the right number. It cannot show that the method runs in 2^o(n) time. Anthropic's paper says of its own approach that it "seems unlikely to yield any general improvement unless n > 10^7", and adds: "Brute force enumeration is already impractical for n = 100". The notes present the script as what it is, a comprehension aid that "complements the Lean formalization".

How it was made. The PR states: "Contributed by Chelsea A. McElveen; implementation and drafting assisted by Claude (Anthropic)." The notes add that "the author is responsible for the content", and both commits carry a co-author line for "Claude Opus 5.5".

Has anyone rechecked the Lean proofs?#

The builds, yes. What the statements mean is a separate question. Two independent rechecks are public:

  • Carlos Toledo's audit. Announced in a comment on the organizers' blog on 28 October, Toledo's report replays both labs' Lean developments with Comparator, Lean's own kernel and nanoda, "a kernel written independently of Lean's". "Both accept both proofs, using only propext, Classical.choice, Quot.sound", the three standard axioms. OpenAI's Lean defines no ETH, so Toledo wrote a textbook ETH in Lean and reports a Lean proof that each lab's statement refutes it in that lab's own machine model. What stays open, in his words: "Two things no kernel can check: that each lab's machine and input encoding match the textbook's …, and that our Lean ETH is the textbook ETH, which is a reading and always will be." His conclusion: "It does not certify that ETH is false." He discloses that his tools "are written with Claude, Anthropic's model, and one of the two claims is Anthropic's", and he reports no affiliation with either lab.
  • Pull request #62. Opened on 29 October and still open, it reports an independent rebuild of OpenAI's Lean development: all 3,977 modules, a check of the axioms, and a comparison of the challenge and solution statements. The PR says plainly that "this is not a comparator run". Replying for the repository on 30 October, Johannes Schmitt welcomed the rebuild and noted that "the repository has no comparator run for family 378 yet". He asked to leave out the PR's reading of what the statement means: "since both readers were language models, it does not belong in the paper's notes."

That reply draws the line this examination keeps returning to. A machine can check that a proof matches its formal statement. Whether the formal statement says what ETH says is a reading, and in that repository a reading by language models alone does not count.

There is also a gap between the paper and its Lean proof. OpenAI's Lean scope note says the formal proof gives a time bound with exponent n(log log n)²/√log n. The paper's sharper exponent, n·log log n/√log n, rests on the natural-language proof alone.

What are the first follow-up papers?#

Within two days, several deposits on Hexagon, a preprint repository for the mathematical sciences, built on the claims. Each carries Hexagon's labels for how much of the text was AI-generated and how much a human has understood.

DepositContributor, dateWhat it says it doesHexagon labels
2610.00574v1Scott Kominers, 27 Oct"a preliminary exposition of a qualitative form of the main result"Mix of human and AI text; human understanding: some parts
2610.00594v1Deep Bhattacharjee, 28 OctReproduces OpenAI's counting algorithm and extends it from counting to weighted sumsMix of human and AI text; some parts
2610.00600v1Isaac Rudich, Louis-Martin Rousseau, 28 OctClaims deterministic factoring in time N^o(1), with a Lean proofMix of human and AI text; some parts
2610.00613v1Xiaoyu Li, 28 OctAsks what the refutation changes for learning theoryPrimarily AI-generated text; some parts

The declarations are frank. Kominers calls his draft "highly preliminary and heavily LLMathed" and writes: "I have read and understood each component individually, but I am still far from having fully 'grokked' the argument as a whole." Rudich and Rousseau write that the ideas and the Lean proof were generated by Claude Opus 5.5; they specified and audited the formal statement, and "we did not read the proof, which is checked by Lean."

The learning-theory paper. Hexagon 2610.00613v1, "What Does the Refutation of the Exponential Time Hypothesis Mean for Learning Theory?", was deposited on 28 October by Xiaoyu Li (the page header shows version 1 as 29 October). Its page carries the labels "Primarily AI-generated text" and "Human understanding: some parts". The provenance statement begins: "This work was produced on 28–29 October 2026 with Claude Opus 5.5 (Anthropic), working as an agent in Claude Code." It goes on: "The submitting contributor posed the question of what the refutation of the Exponential Time Hypothesis means for learning theory, directed the presentation, and chose the title. Claude chose the results, proved them, wrote the text and drew the figures." Separate Claude agents checked citations, "audited the proofs, and reviewed the paper as referees". The PDF's own AI disclosure opens: "This paper was written with Claude Opus 5.5 (Anthropic), working as an agent in Claude Code", and ends: "The author is responsible for the content."

The paper's abstract begins: "Two recent works by OpenAI and Anthropic refuted the Exponential Time Hypothesis (ETH)." It then claims a "locality principle" for when the new algorithms speed up learning, and that "the Sparse Max-SAT Hypotheses of Alman and Vassilevska Williams are false". The provenance statement explains how it uses the two refutations: "as black boxes, quoted as Imported Theorems." So its results stand or fall with the claims it imports. The labels and the provenance statement say who did what. They cannot say whether the imported claims hold. That is the examination's question.

What have named researchers said since?#

Opinions, with their limits stated. Lance Fortnow wrote on his blog on 28 October: "I have not verified the proof myself, but it is safe to assume now that the exponential-time hypothesis is toast."

Ryan O'Donnell, who wrote the exposition that Fortnow suggests reading first, posted it with the line "DISCLAIMER: no idea if it's correct". Its footnote says it was "Produced by odonnell@cs.cmu.edu through interaction with LLMs". Asked about his first reaction to the claim, Williams answered on 27 October: "I asked, 'Are you sure?' They replied that they'd verified it in Lean. I said, 'OK but are you sure?'"

What would count as confirmation?#

No single check. "Is the ETH refutation verified?" breaks into separate questions, each answered by different people with different evidence:

QuestionWho or what can answer itStatus on 30 October
Does the Lean proof check against its own statement?Lean's kernel, Comparator, independent kernelsOpenAI's release says so; Toledo replayed both labs' proofs; PR #62's rebuild of OpenAI's is open
Does the Lean statement say ETH is false?People reading the machine model, the input encoding and the definitionsToledo reports a Lean proof that each statement refutes a textbook ETH in that lab's own model; the step between models "stays informal"; no examiners' reading posted
Does the paper's sharper bound hold?Experts reading the natural-language proofNot formalized, per OpenAI's scope note; no published reading
Do people understand the proof?Expositions, lectures, seminarsDrafts, slides, videos and a recorded lecture; none claims to certify
What do the organizers find?Impagliazzo, Paturi and Williams, with the communityNone posted that we found; a virtual meeting is proposed before the end of 2026

The same questions apply to Anthropic's claim separately: it is a distinct paper with its own Lean development.

The organizers' letter says a result of this significance requires "careful, independent scrutiny and an understanding that others can reconstruct, question, and build upon". By that measure, the work is early. Volunteers have shown that a toy version of the construction computes the right count on small formulas, and that the formal proofs build. The parts that need people, reading the statements and the sharper bound, are where public results are still missing.

What changed on Papex?#

The ETH page lists both claims, OpenAI's and Anthropic's, as their sources state them. Its status is Claimed: Papex shows the status its source gives, not a verdict of its own. With this post, we have added the community notes in PR #60 to the page as a response on OpenAI's claim. Both claims are also on /ai-claims, our list of AI-assisted claims on open problems.

Sources#

Keep reading

All posts

Axiom's Lean formalization of the classification of finite simple groups: what it checks

Axiom says AI agents formalized the classification of finite simple groups in Lean. What the files establish, what Axiom found in the literature, and what still needs people.

Explainer

Why OpenAI withdrew three Hodge conjecture papers: the sign error explained

OpenAI withdrew three AI-produced papers on the Hodge conjecture within two days. A new arXiv note by Lekili and Sheridan explains where the sign error came from.

Explainer

Nivat's conjecture: an AI-found proof in Lean, and what understanding would add

Bryna Kra says new proofs of Nivat's conjecture seem correct but come without understanding. What one public, AI-found Lean proof establishes, and what it leaves to people.

Explainer