Claude Refuted ETH Too: Anthropic's 3-SAT Paper Explained

§ 01What the paper claims#

3-SAT asks whether a formula of three-literal clauses can be satisfied. Checking all 2^n assignments always works; since the 1980s the best algorithms only shrank the base of that exponent, to 1.328^n for deterministic algorithms and 1.308^n for randomized ones. The Exponential Time Hypothesis, posed by Impagliazzo and Paturi in 2001, says no algorithm can get the exponent below some fixed fraction of n.

Claude’s algorithm does. It is deterministic, and it solves the harder counting problem, #3-SAT, in time 2^O(n log log n / sqrt(log n)) by Anthropic’s README. That grows more slowly than 2^(dn) for every d above zero, which is exactly what ETH rules out. The paper’s tools are tensor networks and rank; Nelson’s summary below sketches them.

Two consequences follow from earlier work, by the paper’s own account:

• SETH falls too. The strong hypothesis implies ETH, so refuting ETH refutes it.
• Other problems get subexponential algorithms in theory: Independent Set, Clique, Vertex Cover and Dominating Set in time O(2^(dn)) for every d above zero, and a new circuit lower bound for the class E^NP.

§ 02Two labs, one day#

Jelani Nelson, a Berkeley theorist, wrote on X: “it seems indeed the models even obtained the results on the same day.” He says he and others read Claude’s proof the week before release to improve its exposition, and that “it seems both proofs ultimately get roughly exp(O(n / sqrt(log n))) time with lower order terms in the exponent.”

We covered OpenAI’s announcement, which also claims Kakeya and Yang-Mills results, in OpenAI Claims Yang-Mills, ETH and Kakeya Proofs.

§ 03How it was checked#

The Lean files state two theorems on Mathlib’s Turing machines: that ETH is false, and the paper’s Main Theorem with its time bound. Anthropic says the build took about 8 minutes on 24 virtual CPUs and depends only on Lean’s three standard axioms. Its CI also runs Comparator, which checks the statements against a challenge file and re-checks the proofs with a second, independently written kernel called nanoda.

Lean checks the proofs; it cannot check that the formal statement matches the paper. Anthropic keeps the statement file short for that reason and prints it, with its differences from the paper, in an appendix. The README also notes that Claude Opus 5.5 at high effort can rederive the weaker form of the result from a one-paragraph hint.

§ 04Why nothing changes for real SAT solvers#

The paper is blunt about practice: “Thus our result says nothing about solving formulas in practice.” The improvement hides in constants that only pay off at absurd sizes.

For scale, the paper notes brute force is already impractical at n = 100. Industrial SAT solvers run on heuristics that this result does not touch. In 2019 Ryan Williams put the odds that ETH is true at 70%; the theory community now has two machine-found proofs against it to read.

§ 05What to watch#

• The workshops. Williams, Impagliazzo and Paturi are organizing them; their readout on whether both formal statements capture ETH is the next real signal.
• An Anthropic announcement. As of 08:40 UTC Oct 27 the result lived on GitHub, Hexagon and researchers’ posts, with no post from Anthropic’s main X account.
• Sharper bounds. Both proofs sit near exp(n / sqrt(log n)); a better exponent from either lab, or from humans, would move the story.

§ 06Our conflict#

CellCog’s agents run on Claude Opus 5.5, Anthropic’s model, and Anthropic’s README says that model can rederive the weaker result from a hint, so we have a reason to like this story. We have not checked the proof; every claim here comes from Anthropic’s paper, README and Lean files, and from the researchers quoted.