A subexponential algorithm for counting 3-SAT solutions, refuting the Exponential Time Hypothesis

A 49-page paper authored by Claude gives a deterministic algorithm that counts the satisfying assignments of a 3-CNF formula on $n$ variables in $2^{o(n)}$ time, which contradicts the Exponential Time Hypothesis, and a Lean 4 development in Anthropic's public repository states and proves the refutation against Mathlib's Turing machines using only Lean's three standard axioms.

What was found

The Exponential Time Hypothesis of Impagliazzo and Paturi says there is a constant $\delta > 0$ for which 3-SAT on $n$ variables cannot be solved in $O(2^{\delta n})$ time. The paper gives a deterministic algorithm for the harder counting problem #3-SAT running in $2^{o(n)}$ time, which contradicts it, and a main theorem covering $k$-CNF formulas with $m$ clauses in time $2^{O(\min\{km/\sqrt{\log m},\ k^2 n \log\log n/\sqrt{\log n}\})}$. Every earlier improvement had reduced the exponent by a constant factor rather than removed it: the records the paper cites are $O(1.328^n)$ for deterministic 3-SAT and $O(1.308^n)$ for randomized. The paper states consequences for other NP-complete problems, with Independent Set, Clique, Vertex Cover and Dominating Set on $n$ vertices each solvable in $O(2^{\delta n})$ time for every $\delta > 0$. It says the result was found by an internal Claude research model using 14 million output tokens with no human input, after which Anthropic researchers worked with Claude on the presentation, and it names OpenAI's concurrent result as independent. The Lean development reached the public repository as pull request 31, merged on 27 October 2026 at commit 16a5ce41304fcdaea4e0be7c132e1c361dc26da5 and adding 1,063 files; the README documents a roughly eight-minute build on 24 virtual CPUs, pins Lean and Mathlib at v4.33.1, and prints the axiom dependencies of both headline theorems as exactly propext, Classical.choice and Quot.sound.

Novelty check

Searched arXiv on 2026-10-27. The hypothesis was standing rather than previously refuted: abs:"exponential time hypothesis" AND abs:"refute" returned 18 records, every one of which assumes ETH to derive lower bounds rather than attacking it, the most recent being "Independent Set Hardness in Graphs of Bounded Twin-Width and Low-Radius Merge-Width" of 30 June 2026; ti:"exponential time hypothesis" returned 6 and abs:"3-SAT" AND abs:"subexponential" returned 7, with no prior claim of a subexponential 3-SAT algorithm among them. The paper's own account of the prior art agrees, citing $O(1.328^n)$ deterministic and $O(1.308^n)$ randomized as the records. Nothing in this registry duplicates it, but it sits directly beside 2026-10-05-3sum-apsp-hypotheses, in which an internal Anthropic model refuted the 3SUM and APSP hypotheses, two other load-bearing conjectures of fine-grained complexity, three weeks earlier. The live novelty question is therefore not priority against the literature but concurrency: OpenAI released a refutation of the same hypothesis on the same day, recorded here as 2026-10-26-eth-refuted-openai, and this paper cites that work as independent and concurrent rather than as prior.

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

whataifound.org. (2026). A subexponential algorithm for counting 3-SAT solutions, refuting the Exponential Time Hypothesis. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-26-eth-refuted-claude

@misc{whataifound-anthropic-2026-claude,
  title        = {A subexponential algorithm for counting 3-SAT solutions, refuting the Exponential Time Hypothesis},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Anthropic. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-26-eth-refuted-claude}
}

Related findings

← All computer science findings in the registry