Anthropic says Claude also refuted the Exponential Time Hypothesis, hours after OpenAI

The skim

• Hours after OpenAI said its AI had disproved the Exponential Time Hypothesis, Anthropic posted its own claimed refutation, written up by Claude and checked in Lean.
• Anthropic says an internal Claude model found the core algorithm on Oct. 16 with no human input, and that it worked "independently and concurrently" with OpenAI.
• Neither proof has been peer-reviewed. Anthropic's own paper says the result "says nothing about solving formulas in practice."

What happened

On Monday OpenAI said an internal model had refuted ETH, the assumption that a classic logic puzzle called 3-SAT can't be solved much faster than by checking an exponential number of possibilities. (Our morning story has the background.) At 11:07 p.m. ET that night, Anthropic added a folder to its formal-math repository on GitHub with a paper titled "A 2^o(n) Time Algorithm for 3-SAT," credited to "Claude, Anthropic."

The paper claims a deterministic algorithm that does more than refute ETH: it counts every satisfying assignment of a 3-SAT formula in sub-exponential time. Its provenance note says the core algorithm "was found on October 16 by an internal Claude research model with 14M output tokens and no human input," and that Anthropic researchers then worked with Claude on the write-up. It adds that, "independently and concurrently, an internal model at OpenAI claims to have proven a similar result."

The Lean 4 formalization was also written by AI models, and the repo's checks re-verify it with a second, independently written proof kernel. Anthropic is upfront about the limit of that check: its README says "Lean checks the proofs, but no machine checks that this file says what the paper says." It also claims Claude Opus 5.5 can rederive the basic refutation, without the sharper bound, from a one-paragraph hint.

Why it matters

Two rival labs landing on the same refutation of a conjecture first proposed in 1999, on the same day, makes the claim harder to wave off. It also raises the stakes if it's wrong. In a literature search run by Claude, Anthropic says it found more than 800 papers that prove at least one result only under ETH or a stronger hypothesis it would also knock down, such as SETH. The paper says the related Orthogonal Vectors hypothesis, which supports many fine-grained lower bounds, survives.

Nothing changes for anyone running a SAT solver today. Anthropic's paper says its bound only beats brute force on astronomically large inputs, that its approach seems unlikely to help on any formula with fewer than about 10 million variables, and that brute force is already impractical at 100. MIT's Ryan Williams, who is helping lead the outside review with ETH's co-proposers Russell Impagliazzo and Ramamohan Paturi, told TechCrunch that OpenAI checked whether its algorithm breaks any cryptosystems and was "reasonably confident" it doesn't.

There's rivalry here too. TechCrunch reports that Anthropic mathematician Levent Alpöge suggested OpenAI's results built on pre-existing work before Anthropic published its own. Anthropic also just filed to go public, so a headline research result arrives at a useful moment.

What's next

The review group's open letter lists Anthropic's paper alongside OpenAI's, WebProNews reports, and the organizers have proposed a virtual meeting before the end of the year. The question to watch is whether human experts can follow either proof well enough to explain it, not just whether Lean accepts it.

Sources: Anthropic on GitHub (paper and Lean proof), Hexagon preprint, TechCrunch and WebProNews.