Summary
Anthropic says an internal research Claude model found a deterministic subexponential-time algorithm for 3-SAT, contradicting the Exponential Time Hypothesis. Its repository includes a Lean 4 formalization and describes the result as asymptotic, not a practical solver.
Anthropic’s formal-math repository describes a deterministic algorithm for 3-SAT whose running time is subexponential in the number of variables. The company says the result was discovered by an internal research Claude model and that AI models wrote its Lean 4 formalization. If the algorithm’s stated bound is correct, it refutes the Exponential Time Hypothesis (ETH), a central conjecture in computational complexity.
Why the time bound conflicts with ETH
3-SAT asks whether a Boolean formula made from clauses of three literals has any satisfying assignment. ETH is the conjecture that no algorithm can solve 3-SAT in time exponential in a sublinear function of the number of variables—in other words, that a general subexponential-time algorithm does not exist.
Anthropic’s repository gives a more specific bound for the harder counting problem, #3-SAT: counting the satisfying assignments of a formula. It reports a running time of 2^{O(n log log n / √log n)}, where n is the number of variables. Because the exponent grows more slowly than n, this is a subexponential bound. An algorithm that counts assignments can also decide satisfiability by checking whether the count is zero, so the reported counting result implies a subexponential decision algorithm.
The repository’s outline says the proof works through tensor-network contractions on complete graphs. In broad terms, a tensor network represents a computation as connected mathematical objects whose shared indices are summed over. The outline describes decomposing SWAP operators and grouping network nodes by rows or columns to control the contraction cost. The repository points to a paper for the full argument; its README presents this sketch as a condensed description rather than a complete derivation.
What the Lean formalization checks
The repository includes a Lean 4 formalization of the result, using Mathlib’s framework for Turing machines. It identifies formal statements corresponding to the claim that ETH is false and to the paper’s main theorem. The repository also documents a fuller check, run by its CI, that compares theorem statements with a challenge file and rechecks proofs using nanoda, a separately written kernel.
The repository distinguishes checking a formal proof from checking how its formal statement corresponds to the paper. It says the short Lean file does not itself machine-check that correspondence; the paper’s Appendix E prints the file and explains differences, while a proof index maps numbered paper statements to their Lean counterparts. This makes the formalization a significant part of the research artifact, while leaving readers a specific bridge between the paper’s mathematics and the formal statements to inspect.
Anthropic explicitly characterises the result as purely asymptotic: it says nothing about solving 3-SAT formulas in practice. The claim is about the theoretical limits of algorithms, not a new SAT solver demonstrated on real-world workloads.