Anthropic Says Claude Refuted the Exponential Time Hypothesis

Anthropic says an internal Claude research model refuted the Exponential Time Hypothesis, following OpenAI's similar claim, according to TechCrunch. The hypothesis states that no algorithm can solve 3-SAT in subexponential time.

Anthropic's algorithm solves 3-SAT with n variables in 2^o(n) time. It also counts the satisfying assignments for the harder #3-SAT problem in time 2^(O(n log log n / √log n)). The result is asymptotic and does not provide a practical way to solve formulas faster.

Anthropic published the paper and a Lean 4 formalization on GitHub, both written by AI models. Lean checks the formal proofs using three standard axioms, while a second kernel called nanoda provides an additional check. The repository notes that these checks do not independently confirm that the formal statements match every claim in the paper.

Anthropic released its result hours after mathematician Levent Alpöge, who works at Anthropic, suggested that OpenAI's solution built on existing work. MIT professor Ryan Williams, who has criticized OpenAI's earlier proof releases, is organizing the computer science community's review of the claims.