Anthropic posts its own ETH refutation, found by Claude and checked in Lean 4
Anthropic published a paper by Claude claiming a deterministic algorithm that solves 3-SAT, a classic logic puzzle, faster than the Exponential Time Hypothesis allows, which would refute it. The result was discovered by an internal research Claude model, and the Lean 4 formalization, a machine-checked proof, was also written by AI models. Anthropic says the result is purely asymptotic and says nothing about solving formulas in practice. Lean checks the proofs, but not that the formal statement matches the paper.