A 2^{o(n)} Time Algorithm for 3-SAT

What was already known

Impagliazzo and Paturi formulated ETH. Earlier deterministic 3-SAT bounds retained a fixed exponential base. OpenAI released a concurrent subexponential counting claim on 26 October; this is Anthropic’s separately credited algorithm, not another report of that manuscript.

AI involvement AI-autonomous

The manuscript’s provenance paragraph says the core algorithm was found on 16 October by an internal Claude model using 14 million output tokens and no human input. Anthropic researchers subsequently worked with Claude on presentation.

Importance Major

Would refute a central hardness hypothesis used across algorithms and complexity, while giving an explicit exact-counting time bound.

Limitations

The counting target excludes repeated clauses, unused variables and the stated small-input cases; these can be handled separately, and the ETH decision statement covers all encoded 3-CNF instances. Conversion to other machine models is explained outside the Lean theorem. The algorithm is asymptotic and supplies no practical SAT solver or polynomial-time solution of NP-complete problems. The source reports a concurrent discovery; equivalence of the two labs’ mechanisms has not been established here.

Technical verification Formal (Lean 4)

The source reports completed Lean verification of MainResults.ethIsFalse and mainTheorem. The exact-commit verify (eth) job succeeded. MainResults and the Comparator configuration specify the Mathlib TM2 model, finite stack alphabets, encodings, quantifiers and only propext, Quot.sound and Classical.choice. This is source-reported checking, not a local replay.

Formal checking

Checker: Anthropic: Lean 4.33.1 and Comparator/nanoda CI
Scope: One deterministic finite-alphabet Mathlib TM2 machine exactly counts the satisfying assignments of k-CNF formulas with k≥1, m≥2 distinct clauses and n≥4 occurring variables in time 2^{O(min{k²n log log n/√log n, km/√log m})}, with base-two logarithms and an absolute hidden constant. A separately formalized decision statement refutes ETH.
Basis: Reported by the linked checker
Check date: 2026-10-27

Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Few is the default when evidence for a higher level is insufficient. The manuscript and condensed hint are AI-produced. A completed named human explanation of the central tensor-network contraction argument is not documented in the reviewed sources.

Correction and publication history

2026-10-28 · publication

Newly reviewed source-backed algorithm with contribution-specific AI attribution and checking limits.

Read this published revision