Anthropic Says Claude Refuted the ETH Hypothesis

An internal Claude model has found an algorithm for 3-SAT that would refute the Exponential Time Hypothesis, one of the central assumptions of computer science, Anthropic claims in a preprint posted on Hexagon on 27 October. The company has also put the paper and a machine-checked proof written in the Lean language on its GitHub.

The claim arrives a day after OpenAI said one of its own models had refuted the same hypothesis. Anthropic acknowledges this in its paper: “Independently and concurrently, an internal model at OpenAI claims to have proven a similar result.” Neither lab’s result has yet been peer reviewed, and no outside expert has published a review of Anthropic’s version.

In brief

Anthropic says an internal Claude model found a deterministic algorithm that solves 3-SAT in time below any exponential, refuting the Exponential Time Hypothesis.
The proof is formalised in Lean 4, but Anthropic’s README says the result “is purely asymptotic” and that no machine checks the Lean statement matches the paper.
OpenAI made a similar claim a day earlier; neither has been independently reviewed.

What 3-SAT and ETH actually are

3-SAT is a puzzle about switches. You have n variables, each true or false, and a list of rules. Each rule says that at least one of up to three conditions must hold, such as “x1 is true, or x4 is false, or x7 is true”. The question is whether any setting of the switches satisfies every rule at once. The obvious method tries all 2^n settings, which doubles in cost with each extra variable. The paper says the best deterministic algorithms until now ran in about 1.328^n steps, and the best randomised ones in about 1.308^n: faster, but still exponential.

The Exponential Time Hypothesis, proposed by Russell Impagliazzo and Ramamohan Paturi, says that exponential growth cannot be avoided. Some fixed rate, however small, always remains. Anthropic’s paper says its algorithm beats every such rate, running in 2^o(n) time, which means the exponent grows more slowly than any fixed fraction of n. The README gives the precise bound for the harder counting version, #3-SAT, as 2^O(n log log n/√log n). The paper’s key words point to the method: tensor networks and rank.

Refuting ETH would not settle P versus NP, and the paper is careful on that point. “Our result does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems,” it says. It also says the result refutes the stronger hypothesis known as SETH, but not the Orthogonal Vectors hypothesis, on which many other hardness results rest.

A proof that only bites at astronomical sizes

The README’s opening caveat is blunt: “The result is purely asymptotic and says nothing about solving formulas in practice.” The paper puts numbers on that. For typical formulas with five rules per variable, its proven bound only beats brute force once n exceeds 10^10,000. Its bound stated in n alone needs n above 10^10. Brute force is already impractical at n = 100, the paper notes.

The stakes are theoretical, but large. In a literature search Claude carried out, the authors say they found “more than 800 papers” that prove at least one result only by assuming ETH or a hypothesis that implies it. If the refutation holds, those results lose that footing. The paper also says it implies faster algorithms for Independent Set, Clique, Vertex Cover and Dominating Set, and a new circuit lower bound, through earlier theorems by MIT’s Ryan Williams and others.

Who did the work, by Anthropic’s account

According to the provenance statement, “The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input.” Anthropic researchers then worked with Claude on the presentation. Hexagon labels the paper “Primarily AI-generated text”, with human understanding of “some parts”. The README says the Lean 4 formalisation “was written by AI models”, and that Claude Opus 5.5, at high effort, can rederive a weaker form of the result from a short description.

The Lean build, by Anthropic’s account, takes about eight minutes on 24 virtual CPUs and uses only Lean’s three standard axioms. The repository’s automated checks also re-run the proofs on a second, independently written checker. But the README adds a caveat that matters more than any build log: “Lean checks the proofs, but no machine checks that this file says what the paper says; the file is kept short so that a reader can check this.” The repository is labelled a research artefact that is not maintained and does not accept contributions.

Two labs, one date and one open question

The most striking detail is the timing. Anthropic says its model found the algorithm on 16 October, the same date OpenAI gave for its own discovery. The two papers’ stated running times are close but not identical, and Anthropic calls OpenAI’s result only “similar”. If both hold, two separate systems overturned an assumption that, by the paper’s own count, hundreds of papers rely on. The paper itself recalls that Williams put the chance of ETH being true at 70% in 2019. Two independent routes would make an error less likely, but only once each has been checked on its own terms.

That checking is the gap. OpenAI chose named outside experts to “shepherd” its result, which drew criticism from an advisory panel of mathematicians. Anthropic has taken a different route: a public preprint, an open licence and a proof anyone can rebuild, with no named reviewers. That fits the community-led approach behind the $15m Simons Foundation programme that Anthropic co-funds, but it also means nobody has yet publicly vouched for the work. The Lean caveat is the practical test. A short statement file means a human expert can read it in an afternoon and confirm that the formal theorem really says “ETH is false” in the accepted sense. Until someone does, this is a formally checked claim, not an established result. It joins a run of AI-assisted maths claims, from Microsoft’s KLS conjecture work to DeepMind’s AlphaProof Nexus and a preprint crediting Shanghai AI Lab’s Intern-S2, where outside review has trailed the announcement.

The next signal will come from complexity theorists who read the statement file and the 2^o(n) argument against the original definition. Whether either lab’s paper is submitted to a journal or conference is not yet stated.