Anthropic posted a preprint on October 27, 2026 claiming a deterministic subexponential-time algorithm for 3-SAT, a result that would refute the Exponential Time Hypothesis if it survives review.
In the Anthropic preprint, the claimed runtime is 2^o(n), and the paper says the same approach also gives a subexponential result for #3-SAT. Anthropic says the core algorithm was found on October 16 by an internal Claude research model using 14M output tokens with no human input, before researchers worked with Claude to develop the paper.
Anthropic also released a Lean 4 artifact alongside the preprint. Its README says Lean checks the proofs, but no machine checks that the Lean statements exactly match the paper. The same repo also says the result is purely asymptotic, not a claim about practical SAT solving.
The main caveat is that this is still an unreviewed claim. The paper and formalization are public artifacts, but they do not replace outside scrutiny from complexity theorists.