Anthropic says Claude model refuted the Exponential Time Hypothesis with a 3-SAT algorithm

Anthropic has posted a preprint presenting a deterministic algorithm for 3-SAT on n variables that runs in 2^{o(n)} time, which the paper says refutes the Exponential Time Hypothesis (ETH). The company says the core algorithm was found by an internal Claude research model, and that the result has been formalized in Lean 4.

The paper went up on hexagonmath.org on October 27. OpenAI had announced a similar claim a day earlier, so this is a photo finish in a race nobody told the referees about.

What the paper claims

Subexponential time for 3-SAT is exactly what the hypothesis said should not exist. ETH was proposed in 1999 and has stood as a pillar of theoretical computer science for almost 30 years. Anthropic says its algorithm does more than decide satisfiability: it also solves the harder counting problem #3-SAT, returning the number of satisfying assignments.

The provenance line is the part worth reading slowly. The paper states: "The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input." Anthropic researchers then worked with Claude to improve the presentation, and that produced the paper.

So the discovery is dated October 16, the preprint October 27. Eleven days between a claimed result and a public manuscript is fast. It is also not peer review.

OpenAI announced first. Both give October 16.

According to The Latent, OpenAI announced on October 26 that its models produced a proof that ETH is false. OpenAI says its models generated the natural-language disproof on October 16, the same date Anthropic gives, and formalized it in Lean the next day. Both are in a public GitHub repository.

OpenAI also unveiled two other AI-generated results the same day: a proof of the local smoothing conjecture in all dimensions, and an existence proof for certain quantum field theories, including Quantum Chromodynamics and pure Yang-Mills theory. I will leave those for people with the relevant degrees and a free weekend.

There is a side plot. Anthropic mathematician Levent Alpöge suggested that OpenAI based its solutions on pre-existing work. The coverage does not say which work he means. The cited coverage does not include a comparison of the two proofs.

OpenAI says an external group is examining its work, led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego (two of the hypothesis's original proposers, per The Latent) and Ryan Williams of MIT. WIRED places the original proposers at UC Santa Barbara instead. One of the two outlets has a geography problem, and it is a small one next to the proof.

Independent checks are still pending

Both firms have published their proofs on GitHub, in natural language and in the Lean format.

The results have been formalized in Lean, but WIRED reports that researchers have not yet independently verified or fully understood the proofs. OpenAI's effort so far includes a Google form asking for volunteers and feedback, plus a commitment to fund a conference.

Context does not help OpenAI's credibility. WIRED notes that earlier this month the company put 722 manuscripts on 400 problems on GitHub, which annoyed academics who say the volume makes the results hard to digest. Several of those documents contained errors.

What it would change, and what it would not

The academic fallout, if the result holds, is large. UC Santa Barbara professor Daniel Lokshtanov told WIRED that if confirmed, the result will render him "galactically wrong" and make around 50 of his published papers either "pointless" or in need of a revisit.

The practical fallout is where the headlines and the paper part ways. The Information ran a paywalled story headlined "Encryption Under Siege? OpenAI, Anthropic Disprove Key Cryptography Theorem." Lokshtanov told WIRED that this particular result doesn't directly affect cryptography, though "it should definitely scare some cryptosystem designers." Anthropic itself, per The Latent, says: "The result is purely asymptotic and says nothing about solving formulas in practice."

That is a refutation with no stated implementation. The announcement gives no runtime on any real formula, and the paper's claim is about how running time grows, not about any solver you could run tonight. Williams was candid: "At the current rate of progress, it's plausible we could see a serious update on practical SAT solving within the next 12 months. Or we might not see anything like that. I really don't know."

What to watch

• Independent verification. Whether outside computer scientists confirm that both firms' Lean formalizations match the theorems claimed.
• The hidden constants. Whether either algorithm has any practical efficiency or stays purely asymptotic.
• The priority dispute. Which pre-existing work Alpöge had in mind, and whether the two proofs are really independent.
• The salvage operation. Which conditional hardness results survive under alternative assumptions, and which are gone.

Two labs, one date, one hypothesis, and outside checks still pending. Until they land, this is a claim with unusually good paperwork.