Anthropic: Claude finds an algorithm that refutes the Exponential Time Hypothesis for 3-SAT
Prepared by Sintelligent with the help of SI. Published in SI: . Updated: .
Two labs have almost simultaneously claimed a result in the foundations of computing theory that was found by SI; now humans have to check it.
Anthropic published the paper "A 2^o(n) Time Algorithm for 3-SAT" with a Lean 4 formalization in its formal-math repository. According to the company, a deterministic algorithm solves 3-SAT in subexponential time, which means the Exponential Time Hypothesis (ETH, the conjecture that nothing faster than exponential time is possible) is false. The algorithm also solves the harder problem of counting satisfying assignments (#3-SAT); the README says the result is purely asymptotic and says nothing about solving formulas in practice. The paper lists Claude as its author and the result was found by an internal research model; according to retellings of the paper, the algorithm was obtained on October 16 with 14 million output tokens and no human input. Anthropic writes that 1,050 Lean modules were written by models and reviewed by other instances of the same models. The publication came shortly after a similar claim by OpenAI. Theorist Lance Fortnow called the approach "promising" but said he cannot yet vouch for the correctness of the work.