Anthropic has put a paper and a Lean 4 proof on GitHub claiming that an internal research Claude model found a fast algorithm for 3-SAT, which would refute the Exponential Time Hypothesis. It arrives within a day of OpenAI’s own claim to have disproved the same hypothesis, so two labs are now saying their models did what theorists have failed to do for decades. Neither claim has been confirmed by outside experts.
3-SAT is a logic puzzle. You get a long list of yes-or-no switches and a pile of rules, each rule involving three switches, and you must decide whether some setting of the switches satisfies every rule at once. For the best known methods, each extra switch roughly doubles the work, which is why big instances become hopeless. The Exponential Time Hypothesis, or ETH, is the bet that no method can ever escape that doubling. Many results in other areas of computer science take the bet as a starting assumption.
The repository, anthropics/formal-math, describes a deterministic algorithm whose running time for 3-SAT, with n switches, is 2 to the power of o(n). In plain terms, the work grows more slowly than any fixed exponential rate. It also handles the harder task of counting every satisfying setting, in a time the page writes as 2 to the power of order n log log n, divided by the square root of log n. Anthropic credits the discovery to an internal research Claude model and lists the paper’s author as “Claude (Anthropic)”. The Lean code, it says, was written by AI models.
The repository is blunt about limits on usefulness. The result is purely asymptotic, it says, and tells us nothing about solving real formulas in practice. A running time that wins only as n grows without bound can lose to today’s ordinary solvers on every formula anyone will actually meet. Anthropic labels the folder a research artifact and says it will not be maintained or take outside contributions.
On verification, the page is more careful than most announcements. Lean checks the proofs, but the repository admits that no machine checks that the short file stating the theorems, MainResults.lean, says what the paper says. Anthropic kept that file small so a human reader can do the comparison. A full build took Anthropic roughly 8 minutes on a 24-core virtual machine, with the largest process near 7 GB of memory, and the proofs rest only on Lean’s three standard axioms. Two warnings about unfinished proofs come from a separate file that states the theorems without proofs, for a deeper check. That check, which runs in the repository’s continuous integration, compares the statements against that file and has a second checker, written separately and called nanoda, go over the proofs again.
One more detail shows how the lab sees the work. The page includes a condensed description of the key idea, written so an AI model can rebuild the argument from it, and says Claude Opus 5.5, run at a high setting, can reconstruct the refutation from that summary. The reconstruction is weaker than the headline, though. It reaches only the claim that for any positive δ, 3-SAT can be solved in about 2^(δn) steps. The tighter figures quoted above are out of its reach. A Hexagon link for the paper is listed as still to come.
The comparison with OpenAI is worth drawing. OpenAI’s route runs through named academics at UC San Diego and MIT who were asked to examine its proof. Anthropic’s route, for now, is a public folder and an invitation to run the build yourself. Both lean on Lean, and both still need someone to confirm that the formal statement means what the abstract says.
Anyone whose work assumes ETH, from graph algorithms to databases, now has two claims to weigh, and Anthropic’s is the one a skeptic can test directly: the build runs from a handful of commands and the statement file is short enough to audit by hand.
Published in Anthropic’s public GitHub repository anthropics/formal-math (folder eth); the source gives no publication date.
