ANTHROPIC'S CLAUDE REFUTES THE EXPONENTIAL TIME HYPOTHESIS, WITH A LEAN PROOF

Summary from the TLDR AI newsletter

Anthropic says an internal research Claude model found, with no human input, a deterministic algorithm that counts the satisfying assignments of 3-SAT formulas in 2^O(n log log n/√log n) time, which would make 3-SAT subexponential and refute ETH. This repository holds the paper and a Lean 4 formalization written by AI models that builds in about 8 minutes, though Anthropic notes no machine checks that the Lean statement matches the paper and the result says nothing about practical SAT solving. It landed hours after OpenAI's own ETH refutation.