Hours after OpenAI announced that one of its internal models had refuted the Exponential Time Hypothesis (ETH), Anthropic has published its own paper making the identical claim: Claude, working independently, found a disproof of its own. According to Anthropic, Claude’s version of the result traces back to the same date as OpenAI’s, October 16, with both labs apparently arriving at the same conclusion without any knowledge of what the other was doing.
The paper, titled “A 2^o(n) Time Algorithm for 3-SAT,” lists the author simply as “Claude, Anthropic.” It presents a deterministic algorithm that solves 3-SAT — and the harder counting version of the problem, #3-SAT, which asks not just whether a solution exists but how many there are — in what’s known as subexponential time. That directly contradicts the Exponential Time Hypothesis, a nearly 30-year-old conjecture proposed by computer scientists Russell Impagliazzo, Ramamohan Paturi, and Francis Zane, which held that no algorithm could solve 3-SAT meaningfully faster than brute-force search as the number of variables grows.
According to Anthropic researcher Levent Alpoge, who shared the result on X, the core algorithm was found on October 16 by an internal Claude research model using 14 million output tokens, with no human input involved in the discovery itself. Anthropic researchers then worked with Claude to refine how the result was presented, which became this paper.
Buried in the footnotes of its own paper
Anthropic’s paper doesn’t frame this as a race, but it does directly acknowledge OpenAI’s work. In its provenance section, the paper states plainly that an internal model at OpenAI “claims to have proven a similar result,” citing OpenAI’s preprint from the same week. The two results appear to have been produced completely independently, by two different labs, using two different AI systems, arriving at the same conclusion about the same thirty-year-old conjecture within what looks like the same window of days.
Like OpenAI’s version, Claude’s disproof has been formalized in Lean 4, the proof assistant that checks mathematical logic step by step rather than relying purely on human reviewers. Anthropic says the proof was verified not just by Lean’s own kernel but by an independently built checker called nanoda, and that the entire development — all 1,050 Lean modules — was built from scratch on top of Mathlib, Lean’s community-maintained mathematics library. This isn’t Anthropic’s first high-profile Lean formalization; Claude previously produced a computer-checked formalization of Fermat’s Last Theorem in 11 days earlier this year.
One detail in the paper’s own appendix is worth flagging: Anthropic states that the Lean development “was written by AI models and reviewed by other instances of the same models,” and that “at the time of writing no person is known to have checked it.” The paper also notes its own constant factor isn’t made explicit. In other words, the formal verification machinery has confirmed the logic is internally consistent, but a human mathematician fully working through Claude’s proof by hand hasn’t been reported yet, at least not according to the paper itself.
What the algorithm actually does, and doesn’t do
As with OpenAI’s result, the significance here is almost entirely theoretical. Claude’s algorithm refutes both the ETH and its stronger cousin, the Strong Exponential Time Hypothesis (SETH), since SETH implies ETH. The paper also shows this has knock-on effects: it implies faster theoretical algorithms for a family of related problems, including Independent Set, Clique, Vertex Cover, and Dominating Set, and it strengthens a known result in circuit complexity by showing a certain class of problems cannot be solved with simple, linear-size Boolean circuits.
What it doesn’t do is bring the field any closer to resolving P vs NP, computer science’s most famous open problem, and the paper is explicit that it yields no practical algorithms for solving these problems faster in the real world. The improvement is, in the authors’ own words, purely asymptotic: for a typical 3-SAT formula, their bound doesn’t actually beat simple brute-force search until the number of variables exceeds roughly 10 to the 10,000th power, an number so large it has no bearing on any computation anyone could ever run. Brute-force search already becomes impractical around 100 variables, so as the paper puts it, the result “says nothing about solving formulas in practice.”
There’s also a more immediate consequence for the field of theoretical computer science itself. Claude’s own literature search, cited in the paper, found more than 800 existing papers whose results depend on the ETH or a related hypothesis like SETH being true. If the disproof holds up to scrutiny, none of those underlying problems suddenly become easy to solve, but the formal justification many of those papers relied on no longer stands, and researchers will need to work out which results can be rebuilt on different foundations.
The timing makes for an unusual moment in AI-driven mathematics: two frontier labs, working in isolation, both converged on disproving the same conjecture almost simultaneously, each catching the other’s result only after the fact and tucking an acknowledgment into a reference list.