Anthropic Says Claude Also Refuted ETH, Using 14M Tokens

Anthropic published a paper dated 26 October 2026. It says an internal Claude research model disproved the Exponential Time Hypothesis (ETH). This is the same idea that OpenAI said its own AI system had disproved on 26 October. The paper says Claude found the main algorithm on 16 October, using “14M output tokens and no human input.”

The paper is called “A 2^o(n) Time Algorithm for 3-SAT” and credits Claude and Anthropic. On 27 October, Anthropic added the paper and a formal proof written in Lean 4 to its public mathematics repository on GitHub. The paper directly mentions OpenAI’s work: “Independently and concurrently, an internal model at OpenAI claims to have proven a similar result”.

Video explainer

A Business Engineer video explains the two labs’ claims about ETH and the events behind them. It is narrated using our published articles.

What Anthropic’s Paper Says

The paper presents a deterministic algorithm that solves 3-SAT for n variables in a time that grows more slowly than any fixed exponential rate. This is written as 2 to the o(n). The paper also says the algorithm counts the number of satisfying assignments, which is the harder problem known as #3-SAT.

3-SAT asks whether a formula made of true-or-false variables can be satisfied. The Exponential Time Hypothesis, proposed by Impagliazzo and Paturi, says that solving 3-SAT requires exponential time. The paper says the best previous deterministic algorithm took O(1.328ⁿ) time, while the best randomized algorithm took O(1.308ⁿ) time.

The paper says its result also disproves the stronger Strong Exponential Time Hypothesis (SETH), but it does not disprove the Orthogonal Vectors hypothesis. Many lower bounds in fine-grained complexity theory rely on these hypotheses. The paper also reports that Claude searched the research literature and found more than 800 papers that prove at least one of their results only if ETH, or another hypothesis that implies ETH, is true.

What Was Posted on X

On 27 October 2026 at 04:00 UTC, Levent Alpöge, whose X profile lists Anthropic, posted a passage from the paper explaining how the result was produced. It says the main algorithm “was found on October 16 by an internal Claude research model with 14M output tokens and no human input”. His post linked to the eth folder in Anthropic’s formal-math repository. This article quotes the same passage from the paper itself.

Chubby (@kimmonismus) posted this 29 minutes later: “An internal Anthropic model also refutes the ETH. With only 14m Output tokens and already on October 16th.” The line “Suddenly everything at once” expresses the poster’s own opinion. The date of 16 October matches the date OpenAI gives for its own disproof.

Andrew Curran posted at 04:20 UTC: “This is extremely confusing, but an internal Claude research model also independently refuted the Exponential Time Hypothesis on October 16, with 14M output tokens and no human input.” Curran called the situation “extremely confusing” but did not explain why.

At 05:54 UTC, @choblin29 posted a summary of the release. It said the formal proof covers 1,050 Lean modules and has been checked by Lean and the independent nanoda kernel. It also noted that “no person is yet known to have checked the full formalization.” Appendix E of the paper says all 1,050 Lean modules were built together, that Lean’s kernel and nanoda both accepted the proofs, and that “at the time of writing no person is known to have checked it”.

How Claude Found It, According to Anthropic

“The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input,” the paper says. “Anthropic researchers worked with Claude to improve the presentation, resulting in this paper.”

The repository’s README says AI models wrote the Lean 4 formal proof. Lean checks the proofs against its three standard axioms. But the README warns that “no machine checks that this file says what the paper says”. The file containing the formal statement is kept short so people can check whether it matches the paper.

The README also says Claude Opus 5.5, when run at high effort, can work out the disproof again from a shorter description of the main idea. However, it can recover only the weaker bound, not the sharper bound presented at the top of the paper. Levent Alpöge, whose X profile lists Anthropic, posted the account of how the result was produced on X on 27 October.

What It Does Not Change in Practice

The paper is clear that the result does not make 3-SAT problems practical to solve. It says: “Thus our result says nothing about solving formulas in practice.” For 3-SAT formulas with five clauses per variable, the paper says its time bound does not beat exhaustive search, which takes 2ⁿ time, unless n is greater than 10 to the power of 10,000.

The paper adds that brute-force search is already impractical when n = 100. It also says the result “does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems.”

Connecting the Coverage

On 26 October, we reported that OpenAI says its AI refuted the Exponential Time Hypothesis. OpenAI dates its disproof to 16 October and says it created a Lean formal proof on 17 October. Anthropic’s paper gives the same date for its own discovery. In September, we covered how Claude formalized Fermat’s Last Theorem in Lean. On 6 October, we reported that OpenAI’s internal model generated 722 mathematics papers.

Anthropic’s S-1 filing this month also said that Claude wrote more than 90% of Anthropic’s new code. For details on how the company earns money, see our breakdown of Anthropic’s business model.

The Structural Read

In our reading, the figure of 14M output tokens gives a sense of the scale of the work. The paper says an AI model produced the main algorithm during a run measured in tokens, while Anthropic’s researchers became involved at the stage of improving how the result was presented in writing.

In our reading, Anthropic’s README also makes an important limit clear: Lean checks the formal proofs, but human readers must still check whether the formal statement matches the paper. This is why the file containing the statement is kept short.

In our reading, the practical warning matters for business readers. The paper says the algorithm becomes faster than exhaustive search only for formulas far larger than those used in practice.

Three Implications

FOR RESEARCHERS Anthropic’s paper and Lean files are publicly available under the Apache 2.0 license. The README gives instructions for rebuilding and checking the proofs. Anthropic says the build took about 8 minutes on 24 virtual CPUs.

FOR COMPLEXITY THEORY The paper identifies more than 800 papers that prove at least one result only if ETH, or a hypothesis that implies ETH, is true. It also says the theorem leads to faster algorithms for problems such as Independent Set, Clique, and Vertex Cover.

FOR THE AI LAB RACE OpenAI and Anthropic each say an internal AI model reached the result on 16 October. Anthropic’s paper describes the two results as independent and concurrent.

The Business Engineer Lens

This story relates to the Business Engineer framework The Product Overhang Doctrine.

The framework begins: “In any product cycle, there are two curves to follow. The first is what your underlying technology can do. The second is what your users can actually do with it.”

In our reading, this result sits at the far end of the gap between what technology can do and what people can use. Anthropic’s paper says the algorithm improves on exhaustive search only for formulas far larger than any used in practice. The framework was published in June 2026 and does not discuss this particular result.

What Is Not Established

The paper and README do not name a peer-reviewed publication venue. The README says a Hexagon link is “to appear”. The Lean proofs check the formal statements, but the README itself says that no machine checks whether those statements match the paper. The paper refers to “an internal research Claude model” but does not name the model version used to make the discovery. OpenAI says outside groups will examine its claim. In the paper and README we reviewed, Anthropic does not describe an outside review of its own result.

The Bottom Line

Anthropic’s paper says an internal Claude model disproved the Exponential Time Hypothesis on 16 October, using 14 million output tokens and no human input. This is the same date OpenAI gives for its own disproof. Both labs have provided Lean formal proofs alongside their claims. Anthropic’s paper also says the result has no practical use for solving formulas.

A note on sources. This article is based on Anthropic’s paper, including its title page, abstract, introduction and section on how the result was produced; the README in Anthropic’s formal-math repository on GitHub; a post on X by Levent Alpöge; OpenAI’s announcement of 26 October 2026; and our earlier reporting. We read these materials on 27 October 2026. We have not examined or run the proofs ourselves. We did not contact Anthropic or OpenAI.

Sources: Anthropic formal-math repository, eth/ (README and Lean files), 27 October 2026 · Claude (Anthropic), “A 2^o(n) Time Algorithm for 3-SAT”, paper dated 26 October 2026 · Levent Alpöge on X, 27 October 2026 · OpenAI announcement, 26 October 2026