Anthropic Says an Internal Claude Model Also Refuted the Exponential Time Hypothesis; No Outside Group Has Confirmed It

Anthropic's claim that one of its models refuted the Exponential Time Hypothesis (ETH) is the second such claim from a frontier lab in a single day, and, like the first, it has not yet been checked by anyone outside the company. Anthropic says an internal Claude research model found the core algorithm on October 16 "with 14M output tokens and no human input." Hours earlier, OpenAI had said its own models refuted the same hypothesis, a claim we reported on October 27 without finding independent verification.

What Anthropic says it proved#

The README in Anthropic's formal-math repository states the claim in one line: "A deterministic algorithm solves 3-SAT on n variables in time 2^o(n), which refutes the Exponential Time Hypothesis (ETH)." It says the algorithm in fact solves a harder problem, #3-SAT, which counts the satisfying assignments, in time 2^O(n log log n / √log n). ETH is the conjecture that 3-SAT cannot be solved in 2^o(n) time, so an algorithm with that running time would contradict it.

The paper, titled "A 2^o(n) Time Algorithm for 3-SAT" and dated October 26, is posted on Hexagon as "Contributed by Anthropic." It says the refutation of ETH also refutes the stronger hypothesis known as SETH, but not the Orthogonal Vectors hypothesis. Using a literature search carried out by Claude, the authors say they found more than 800 papers that prove at least one result of their own only under ETH or a hypothesis that implies it.

The paper says Anthropic researchers then worked with Claude to improve the presentation. It also says that "independently and concurrently, an internal model at OpenAI claims to have proven a similar result," and it cites OpenAI's preprint.

What the claim does not cover#

Anthropic is explicit that the result is theoretical. The README says it "is purely asymptotic and says nothing about solving formulas in practice." The paper says the result "does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems," and that its bound does not improve on exhaustive search until the number of variables is far beyond practical sizes. Neither Anthropic's paper nor its README discusses cryptography.

How the proof can be checked#

The Lean 4 formalization, which the README says "was written by AI models," sits in the eth folder of the anthropics/formal-math repository. The README says the proofs depend only on Lean's three standard axioms, and that the repository's automated check also re-runs the proofs through a second, independently written kernel called nanoda. It adds a caveat in its own words: "Lean checks the proofs, but no machine checks that this file says what the paper says." That file, MainResults.lean, is kept short so that a reader can compare it with the paper by hand, the README says.

Who is reviewing it#

WebProNews, citing the two GitHub commit logs, put OpenAI's files in its openai/math repository at 4:52 p.m. ET on October 26 and Anthropic's in its formal-math repository at 11:07 p.m. ET, about six hours apart. The GitHub records we checked show the same times: 20:52 UTC on October 26 and 03:07 UTC on October 27. OpenAI asked Russell Impagliazzo and Ramamohan Paturi of UC San Diego, two of the hypothesis's originators, and Ryan Williams of MIT to lead an outside review. According to WebProNews, the three wrote in an open letter that "our involvement should not be taken as certification of the claim," and the letter lists Anthropic's refutation among its resources, alongside OpenAI's. WebProNews reports that the letter proposes a virtual meeting before the end of the year, and that neither paper has been peer-reviewed.

Limits#

• The result is Anthropic's claim. We found no independent verification of the algorithm or the formal proof, and no peer review.
• We did not run the Lean build ourselves. The README's own caveat applies: the proofs are machine-checked, but whether MainResults.lean matches the paper's statements needs a human reader.
• The account of how the algorithm was found (October 16, 14 million output tokens, no human input) is Anthropic's, from the paper's provenance note.
• The review group's letter and its proposed meeting are reported by WebProNews; we did not read the letter itself.
• The commit times come from WebProNews and from the GitHub commit records we checked; OpenAI's commit was merged into its main branch at 21:18 UTC. WebProNews reports that each company says its model found the result on October 16; we did not check how either company timed its discovery.

Sources#

• Anthropic (GitHub): formal-math, eth README (October 27, 2026)
• Hexagon: A 2^o(n) Time Algorithm for 3-SAT, contributed by Anthropic (October 27, 2026)
• WebProNews: Two AI Labs Claim the Exponential Time Hypothesis Is False, and the Researchers Who Proposed It Are Organizing a Review (October 27, 2026)
• GitHub API: anthropics/formal-math commits (October 27, 2026)
• GitHub API: openai/math commits (October 26, 2026)
• Times of AI: Anthropic Now Also Claims an AI Refutation of the Exponential Time Hypothesis, Hours After OpenAI; OpenAI's ETH, Local Smoothing and Yang–Mills Claims Remain Unverified (October 27, 2026)