Claude killed the same impossible proof — on the same day, unknowing

Hours after OpenAI announced that one of its internal models had disproved the Exponential Time Hypothesis, Anthropic posted its own claimed refutation: a paper titled "A 2^o(n) Time Algorithm for 3-SAT," credited simply to "Claude, Anthropic," with a Lean 4 formalization in its public formal-math repository. Anthropic says an internal Claude research model found the core algorithm on October 16 — the same date OpenAI dates its own discovery — using 14 million output tokens, with no human input in the discovery itself.

The two proofs look like siblings. Both describe a deterministic algorithm that counts the satisfying assignments of a 3-SAT formula in subexponential time, both are machine-checked in Lean, and mathematician Jelani Nelson, who reviewed Claude's proof independently, said both reach roughly the same runtime bound. Claude's version goes one step further: it also refutes the stronger SETH hypothesis and implies faster theoretical algorithms for related problems including Independent Set, Clique, and Vertex Cover.

Neither proof has been peer-reviewed, and Anthropic is upfront about what the machine check does not do: its README says "Lean checks the proofs, but no machine checks that this file says what the paper says." The hypothesis's own proposers — Russell Impagliazzo, Ramamohan Paturi, and Ryan Williams — are organizing the open review of both claims, and Anthropic's paper concedes the result "says nothing about solving formulas in practice."