Anthropic Says Its Own AI Found a Faster Way to Solve a Famously Hard Logic Problem
Anthropic has published a paper credited to its own AI model, Claude, claiming an algorithm that solves the logic problem 3-SAT faster than a long-standing hypothesis says is possible, with a proof a computer can check. The paper and a Lean 4 formalization of its results were added to the company's public formal-math repository on Oct. 27, 2026. The repository's text says the algorithm refutes the Exponential Time Hypothesis. That is the company's claim, not a settled result; whether the hypothesis is false is for specialists now reading the proof to settle.
3-SAT asks whether a long list of either-or conditions on true-false variables can all be met at once; it is the standard reference problem for questions with no known shortcut. The Exponential Time Hypothesis is the assumption that nothing much beats trying the combinations one by one, a premise used widely to argue that other problems are hard.
Per the repository's README, the algorithm in fact handles the harder counting version, tallying how many ways a formula can be satisfied, in time 2^O(n log log n / sqrt(log n)) for n variables. Anthropic states that the result is purely asymptotic, about very large formulas, and says nothing about solving formulas in practice. The company also says an internal research Claude model discovered it and that the paper and the Lean files were written by AI models.
The folder pins Lean v4.33.1 and lists the commands that check it; Anthropic says the build takes about 8 minutes on 24 virtual processors and that its automated testing re-checks the proofs with a second, independently written checker called nanoda.
A machine-checked proof shows the stated theorems follow from the stated assumptions, which is not the same as the result being accepted. The README says no machine checks that its short statement file says what the paper says, and that the file is kept short so a reader can check it.
Anthropic labels the folder a research artifact, not maintained and not accepting contributions. The paper sits in it as a PDF titled A 2^o(n) Time Algorithm for 3-SAT, credited to Claude (Anthropic).
