Two AI labs have published papers claiming that the Exponential Time Hypothesis (ETH) is false. Anthropic’s paper says an internal research Claude model found a deterministic algorithm for 3-SAT that runs in subexponential time. OpenAI’s preprint makes a similar claim for counting solutions to k-CNF formulas, and Anthropic’s paper attributes that work to an internal OpenAI model.
Someone will ask whether encryption is broken or SAT solvers just got faster, and by the papers’ own account the answer is no on both counts. The papers are also a notable test of AI producing research-level mathematics, worth following even for readers who never touch complexity theory.
What the Exponential Time Hypothesis says
3-SAT is the textbook hard problem. You get a formula over n true/false variables, built as an AND of clauses where each clause is an OR of at most three variables or their negations. The question is whether some assignment makes the whole formula true.
Brute force tries all 2^n assignments. Decades of work have chipped away at that. Anthropic’s paper cites the prior record as O(1.328^n) for deterministic algorithms and O(1.308^n) for randomized ones. Those are still exponential, just with a smaller base.
ETH, from Impagliazzo and Paturi, says you can’t do fundamentally better. The paper states it as: there is a constant δ > 0 such that 3-SAT cannot be solved in O(2^(δn)) time. That’s stronger than P ≠ NP: 3-SAT isn’t just non-polynomial, it’s exponential.
Plenty of theory is built on that assumption. Anthropic’s paper says a literature search carried out by Claude found more than 800 papers with at least one result proved only under ETH or a hypothesis that implies it.
What Anthropic claims
The paper is titled “A 2^{o(n)} Time Algorithm for 3-SAT” and dated October 26, 2026. Its claims:
- A deterministic algorithm solves 3-SAT on n variables in
2^{o(n)}time, which would refute ETH. - It also solves #3-SAT, which counts satisfying assignments rather than just deciding whether one exists.
- The runtime bound is
2^{O(km/√log m)}in the number of clauses m, with a bound in n derived through sparsification. - The result was discovered by an internal research Claude model and formalized in Lean 4.
The provenance section says the core algorithm was found on October 16 by an internal Claude research model using 14M output tokens and no human input. Anthropic researchers then worked with Claude on the presentation.
The paper also notes that refuting ETH would refute SETH, its stronger relative, but not the Orthogonal Vectors hypothesis that many fine-grained lower bounds rely on.
What OpenAI claims
OpenAI’s preprint is titled “The Exponential Time Hypothesis is False.” The repository folder is dated October 25, 2026, and the paper itself says it was dated October 17 and revised October 25.
It claims a deterministic algorithm that counts the satisfying assignments of a k-CNF formula for each fixed k ≥ 2, in subexponential time and polynomial space. Because counting also decides satisfiability, that would refute ETH as well.
Anthropic’s paper acknowledges this directly: it says an internal model at OpenAI independently and concurrently claims to have proven a similar result.
Is the Exponential Time Hypothesis false? The two papers side by side
| Anthropic | OpenAI | |
|---|---|---|
| Title | A 2^{o(n)} Time Algorithm for 3-SAT | The Exponential Time Hypothesis is False |
| Date on paper | October 26, 2026 | October 17, 2026, revised October 25, 2026 |
| Claimed algorithm | Deterministic, solves 3-SAT and #3-SAT in 2^{o(n)} time; extends to k-SAT | Deterministic, counts k-CNF solutions for each fixed k ≥ 2 in subexponential time, polynomial space |
| Credited to | Internal research Claude model | Internal OpenAI model, per Anthropic’s paper |
| Formal proof | Lean 4, per the paper | Lean formalization, scope described in OpenAI’s math repository |
| Status | Unconfirmed, awaiting independent review | Unconfirmed, awaiting independent review |
Two independent groups landing on similar claims at the same time is notable. It doesn’t confirm either one. Errors can share a root, and agreement between two unreviewed papers is not peer review.
What the Lean proof does and doesn’t settle
A machine-checked proof sounds final, so read Anthropic’s Appendix E carefully. The paper says both main propositions were proved in Lean 4 on top of Mathlib, and were accepted by Lean’s kernel, by the leanchecker replay tool and by an independently implemented kernel called nanoda. It says the proofs rest on no axioms beyond Lean’s three standard ones.
That is strong evidence the Lean proof follows from the Lean definitions. The paper is just as clear about where that stops. Whether those definitions really say “ETH is false,” no machine can check; it says that is for the reader of the listing to judge. It also says the Lean development was written by AI models and reviewed by other instances of the same models, and that at the time of writing no person was known to have checked it.
What it doesn’t change for working engineers
This section is the one to pass along in the team chat.
- P vs NP. Anthropic’s paper says the result does not bear directly on P vs NP. Subexponential is still far from polynomial.
- Practical solving. The same paper says the result yields no practical algorithms for NP-complete problems. It states that for 3-CNF formulas with m = 5n clauses, the bound doesn’t beat brute force unless n is larger than 10^10,000. Brute force is already impractical at n = 100.
- Your tools. SAT and SMT solvers, package dependency resolvers, schedulers and constraint solvers work on structured real-world instances with heuristics. Nothing in these papers changes how they behave.
- Cryptography. Neither paper claims to break any cryptosystem, and we wouldn’t read one into it.
Headlines will treat “ETH refuted” as “hard problems are now easy.” They’re wrong: the authors themselves describe the result as purely asymptotic.
Why it’s still worth watching
If the proofs hold, this would be one of the clearest examples so far of AI models producing new research-level mathematics, with a formal proof attached in Anthropic’s case. Anthropic’s paper also lists consequences in theory, including faster asymptotic algorithms for problems like Independent Set and Dominating Set, and a circuit lower bound that follows from earlier work by Williams.
Anthropic’s paper notes that in 2019 Williams estimated the chance that ETH is true at 70%. So some experts already had doubts, which makes a refutation less of a shock, but it still has to be checked.
For users of AI coding tools, the provenance is the notable part. Anthropic says the core algorithm came from a model run with no human input, and that both the paper and the Lean development were produced with heavy AI involvement. More claims like this will come, and the hard part shifts to human review.
What to watch for next
- Statements from complexity theorists who have read the arguments in full
- Independent people building and auditing Anthropic’s Lean development, especially its definitions
- Any errata or revisions to either paper
- Independent audits of OpenAI’s Lean formalization, which its repository says proves subexponential exact counting for each fixed k ≥ 2
We’ll update this post if the review status changes. For more on the AI tools themselves, browse our AI coding tools and models coverage or all guides.
Bottom line
Anthropic and OpenAI each claim an internal model refuted the Exponential Time Hypothesis: Anthropic’s with a deterministic subexponential algorithm, OpenAI’s by counting solutions to k-CNF formulas. Both claims are unconfirmed and still need independent expert review. The papers themselves say the result has no practical algorithmic impact and doesn’t settle P vs NP, so it’s an important research claim to follow, not something that changes your systems.
