Anthropic: "A 2^o(n) Time Algorithm for 3-SAT"
3-SAT (and #3-SAT) in time 2^o(n), with ETH defined in Lean and its negation proved.
What was claimed: 3-SAT (and #3-SAT) in time 2^o(n), with ETH defined in Lean and its negation proved.
What Lean states: ETHIsFalse and MainTheorem in MainResults.lean (anthropics/formal-math eth/ at 16a5ce41), Lean v4.33.1; about 152,000 lines — ETHIsFalse (0 < s₃ negated over FinTM2) and MainTheorem for k ≥ 1, m ≥ 2, n ≥ 4 with every variable occurring.
Prose only / the gap: Reduction from general k-CNFs (unused variables, small m/n) to the MainTheorem promise class.
Verification & replays: Toledo (Comparator 24 GiB, nanoda, leanchecker --fresh, C2 bridge); Szeider; Majdoddin. Not replayed by SeamCert.
What the public sources report
Every item below is attributed to the published paper, replay, or commentary that reported it.
| What the Lean proves | ETH is defined as 0 < s₃ over Mathlib FinTM2 machines, and ETHIsFalse is its negation. MainTheorem counts satisfying assignments within ⌊2^{C·min(km/√lg m, k²n lg lg n/√lg n)}⌋ steps with one absolute constant C. [1] |
|---|---|
| Promises in the statement | MainTheorem covers k ≥ 1, m ≥ 2, n ≥ 4 with every variable occurring. Other k-CNFs reduce to that class by standard steps that are not formalized. [1] |
| Machine model | Mathlib's FinTM2 (multi-stack); one machine for every k; space not stated. [1] |
| Input encoding | A duplicate-free clause list in fixed-width binary slots. [1] |
| Kernel checks | Comparator with Lean's kernel, and nanoda (on as shipped), both accept; only the three standard axioms. leanchecker --fresh exit 0 in 3,011 s. [1] |
| Replay cost | Comparator peaked at 24 GiB of memory. [1] |
| Where it beats 2^n | For m = 5n, the proved bound does not improve on 2^n unless n > 10^10000 (the paper's own figure). Evaluating the level recurrence numerically raises this to 2^275616 clauses and 2^(1.7·10^10) variables. [2] |
| Where it beats the best known algorithms | About 2^420 clauses at clause density one (down from 2^33858), and about 2^(8.6·10^9) variables for general 3-SAT. No grid rewrite-and-merge algorithm gains for general 3-SAT below about 2^6000 variables. [3] |
Open specification seams (our reading)
Our reading of the sources above: the places where the formal Lean statement and the informal headline claim can still come apart.
- FinTM2 and the binary slot encoding versus a textbook multitape machine: Toledo reports this step proved in Lean (C2), with three planted wrong variants refused, on a ported copy of the proof in a newer Lean.
- The #ETH consequence covers only the formulas MainTheorem speaks of; the reduction from other k-CNFs is not formalized.
- That the formal ETH is the textbook ETH stays a reading.
Footnotes & Sources
- Carlos Toledo, "Two claimed refutations of the Exponential Time Hypothesis: what was decided, and what was only read"
- Stefan Szeider, "OpenAI's claimed refutation of ETH: exhaustive search below 2^131071" (Zenodo, 27 October 2026)
- Majdoddin, "Lowered crossover points of Anthropic's subexponential 3-SAT algorithm" (arXiv 2610.41622)
- Claude (Anthropic), "A 2^o(n) Time Algorithm for 3-SAT" (Hexagon 2610.00577v1; Lean in anthropics/formal-math, eth/)
Sources read on 7 November 2026. Spotted an error or a newer independent replay? Write to [email protected].