The Claimed ETH Refutation, Explained

On October 16, an internal Claude research model produced a 14-million-token argument that, if correct, refutes the Exponential Time Hypothesis. The paper says the core argument was produced with no human input, and its Lean development was written by AI models.

Eleven days later the argument arrived on Hexagon as a preprint titled A 2^o(n) Time Algorithm for 3-SAT, deposited by Anthropic and credited to “Claude (Anthropic).” The abstract promises a deterministic algorithm that decides 3-SAT on n variables in 2^o(n) time, and that returns the exact number of satisfying assignments, the harder #3-SAT problem, in the same bound. It also says the result “has been formalized in Lean 4.”

No peer review has happened. What did happen, on October 26, was Ryan Williams of MIT posting that an internal OpenAI model had produced a claimed refutation of ETH, and that he, Russell Impagliazzo, and Ramamohan Paturi had been asked to help organize an open, independent examination. The three answered carefully: “Our involvement should not be taken as certification of the claim. A result of this significance requires careful, independent scrutiny.”

That is the state of play: two machine-written manuscripts, a kernel-checked proof file, and the researchers who built the hypothesis standing in front of it declining to wave it through. What follows is what the artifacts establish, what would fall if they hold, and the four checks worth running before you repeat the headline.

What the Preprint Claims

Strip the framing and Theorem 1 of the paper’s PDF is a running-time bound. A deterministic algorithm computes the number of satisfying assignments of a k-CNF formula in time 2^O(min{sqrt(n log log n / log n), k/sqrt(log m)}), where n is the variable count and m the clause count. The paper writes O(.) with the note that it “hides absolute constant.”

To get a sense of the scale, the same paper lists the standing records it displaces: deterministic and randomized decision algorithms whose running time is c^n for a constant base c only slightly above 1, a base that two decades of work has shaved a few percentage points at a time. Every one of those results is a claim about how small that base can be pushed. A 2^o(n) bound says no constant base survives at all.

The provenance paragraph is the one that will be quoted for years: “The result was found on October 16 by an internal Claude research model with 14M output tokens and no human input. Anthropic researchers worked with Claude to improve presentation.” The same paragraph notes an internal OpenAI model claims a similar result independently and concurrently.

Two sentences in the introduction constrain the claim more than the abstract does. “Our result does not bear on P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems.” The section on the bound adds that the approach “seems unlikely to yield any general improvement” short of instance sizes far past anything enumeration can reach, and that brute force is already impractical at sizes small enough that nobody runs a solver that way. In the paper’s own phrasing, the improvement does not appear in practical settings.

Key Takeaways:

• Anthropic deposited A 2^o(n) Time Algorithm for 3-SAT on Hexagon and claims a deterministic exact #3-SAT algorithm in 2^o(n) time. Its own provenance statement dates the core algorithm to October 16 and credits an internal Claude research model with 14M output tokens and no human input.
• ETH here is the Exponential Time Hypothesis in computational complexity. It is not Ethereum, ether, or the ETH ticker.
• An independent examination is led by Russell Impagliazzo and Ramamohan Paturi with Ryan Williams, who wrote that their involvement “should not be taken as certification of the claim.” No peer review has happened.
• The Lean 4 artifact proves the paper’s stated theorems from stated inputs. It does not prove the Lean statements mean what the prose means, and the paper does not claim a person has checked the argument by hand.
• The result is asymptotic only. The paper says its approach is unlikely to yield any general improvement outside instance sizes far beyond anything enumeration can reach.
• If correct it refutes ETH, SETH, Gap-ETH, NSETH, and #ETH. It does not touch the Orthogonal Vectors Conjecture, does not resolve P vs NP, and does not break cryptography.

The Exponential Time Hypothesis, and Why the Acronym Is Not Ethereum

The Exponential Time Hypothesis, and this is the complexity-theoretic hypothesis rather than the cryptocurrency ticker, was posed by Russell Impagliazzo and Ramamohan Paturi in a 2001 paper in the Journal of Computer and System Sciences, with Francis Zane as co-author on the accompanying sparsification work. It asserts that 3-SAT requires 2^Omega(n) deterministic time in the worst case: there exists a constant delta > 0 such that no algorithm decides 3-SAT in O(2^(delta*n)) time.

ETH is a hypothesis, not a theorem. Nobody has proved it and nobody has disproved it, which is why a claimed disproof is a live event and why “ETH is false” still needs a qualifier attached. It is strictly stronger than P != NP: ETH being true implies P != NP, but ETH being false says nothing about whether P equals NP. Leslie Goldberg of Oxford put the boundary plainly to New Scientist: “Assuming that it is confirmed, this is an enormous breakthrough,” and “This doesn’t have a direct impact on P versus NP, so we should not view it as progress towards P versus NP.”

Hundreds of lower bounds are conditional on ETH. Rather than prove a problem is hard, you prove that a fast algorithm for it would yield a fast algorithm for 3-SAT, then invoke the hypothesis. That structure is cheap and it propagates across graph algorithms, parameterized complexity, and database query evaluation. Fedor Fomin of the University of Bergen told New Scientist: “This came as a complete surprise, a shock. Nobody I know expected it.” Fomin said the textbook he wrote would become obsolete if the finding holds.

Counting Is the Harder Target

Decision 3-SAT asks whether a formula has at least one satisfying assignment. #3-SAT asks how many it has. The Anthropic paper states the distinction in its own terms: “#k-SAT, which asks for number of satisfying assignments of k-CNF; in contrast k-SAT only asks whether that number is zero or nonzero.”

Solving the counting problem solves the decision problem, since a positive count means satisfiable. The reverse does not hold. So an exact counter running in 2^o(n) is a strictly stronger object than a decider running in 2^o(n), and a bug in it is harder to notice: an algorithm that occasionally miscounts can still answer “satisfiable” correctly on almost every input, while one that gets the count wrong has failed at the thing it was built to do. The paper also targets #ETH, the counting analogue that OpenAI’s manuscript describes as the assertion that exact counting of 3-CNF requires 2^Omega(n) deterministic time.

The prior best for exact #3-SAT was a constant-base bound of the form c^n with c comfortably above 1. Closing the gap from that to 2^o(n) is the whole size of the claim, and it is why the correctness bar here sits higher than it would for a decision algorithm.

What the Lean 4 Formalization Actually Checks

The anthropics/formal-math repository holds the artifact, and its structure is unusually easy to audit. MainResults.lean states what is proved, on Mathlib’s Turing machines: ETHIsFalse and MainTheorem. That file contains no proofs and imports nothing but Mathlib. The README is candid about the seam: “Lean checks proofs, but no machine checks that this file says what paper says; file is kept short so that reader can check this.”

You can run the check yourself. This is the sequence from the README, and it is what the repository’s CI does:

cd eth
lake exe cache get # download prebuilt Mathlib
lake build # elaborate the proof tree
lake env lean scripts/PrintAxioms.lean

# Expected output:
# 'MainResults.ethIsFalse' depends on axioms: [propext, Classical.choice, Quot.sound]
# 'MainResults.mainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]

# Note: this reproduces the kernel check against Lean v4.33.1 / Mathlib v4.33.1
# under Lean's three standard axioms. It does not compare the Lean statements to
# the paper's prose; that is what Challenge.lean and the comparator step are for,
# and neither is a semantic check. Nor does it test the algorithm's behavior on
# any concrete instance, which the paper's asymptotic framing makes impossible.

The build took about 8 minutes on 24 virtual CPUs with a largest process around 7 GB, per the README, on a toolchain pinned at Lean v4.33.1. Beyond Lean’s own kernel, the repository’s comparator CI runs leanprover/comparator with the nanoda kernel, an independently written Rust re-checker, inside a landrun sandbox, and requires it to print “Your solution is okay!” against the trusted Challenge.lean statements. Two kernels written by different teams catching the same error class is a real safeguard against implementation bugs.

No kernel covers the translation. Alexander Bastounis, Fabian Circelli, and Anders C. Hansen argue in a 2026 arXiv preprint, “Navier-Stokes lost in translation”, that resolving ambiguities in mathematical natural language is arbitrarily high in the Solvability Complexity Index hierarchy, informally harder than any computational problem including the halting problem, and they exhibit cases where an AI-translated Lean proof compiles while failing to correspond to the original prose. The same failure mode applies here: a kernel-verified theorem about a Lean predicate named for #3-SAT is only as good as that predicate’s agreement with the standard definition.

Then there is the human layer. The paper says the Lean development was written by AI models, and the README is explicit that no machine checks whether the Lean statements match the paper’s prose. That is not unique to this artifact. Thomas Hales’s October 9, 2026 guest post on Terence Tao’s blog records that Lean 4 shipped after two pre-release soundness bugs were corrected, that another soundness bug caused by overflow surfaced in May 2025, and that the spring and summer of 2026 were turbulent for the toolchain. Mathlib itself carries nearly 300,000 theorems per Hales. The checker now carries real weight in the pipeline, and it has a bug history like any piece of infrastructure.

What Falls If ETH Fails, and What Survives

The OpenAI manuscript, “The Exponential Time Hypothesis is False”, is more explicit than the Anthropic paper about downstream damage. It states that its Theorem 1.1 “refutes ETH, SETH, Gap-ETH, and NSETH,” and separately that a deterministic 2^o(n) counter also refutes #ETH. Its repository history for October 26 records the claim and the review arrangement in the same breath.

Two precision points that the popular coverage flattened. First, refuting SETH does not refute the Orthogonal Vectors Conjecture. The reduction runs one way: SETH implies OVC, so a disproof of SETH leaves OVC standing, and string lower bounds such as longest common subsequence and regular-expression matching, which follow from OVC, keep their footing. Second, 2^o(n) bounds do not transfer through polynomial-time reductions. The OpenAI paper says a bound of the form 2^(n^o(1)) would be needed for that.

The damage lands on justifications, not on software. Coverage of Anthropic’s paper, for example Tech Times’s write-up, reports that the paper counts more than 800 published results resting on ETH lower bounds. Those results do not become false. They become unproven, and each subfield has to decide whether its specific claim can be rebuilt on another foundation. Clément Canonne of the University of Sydney described the experience to New Scientist: “The web collapsed, and we looked behind. We have no idea why yet.”

Nothing here breaks cryptography. Ryan Williams told TechCrunch he asked OpenAI science lead Dan Roberts directly whether any cryptographic systems were affected, and said OpenAI “checked, and they were reasonably confident that this didn’t imply any breaks.” A subexponential bound on 3-SAT does not by itself give a practical attack on any deployed key size.

The Constant Nobody Has Computed

An asymptotic result with an unquantified constant supports no measurement. The paper writes 2^O(…) and says the O(.) hides an absolute constant, which means there is no function you could evaluate to size an instance for a benchmark. Compare that with the last generation of algorithmic improvements, where the whole point was a constant base you could plug into c^n and evaluate against 2^n at whatever n you cared about.

The paper is direct about the resulting gap. It says its general approach “seems unlikely to yield any general improvement” except at instance sizes far beyond what enumeration can touch, and that brute force is already impractical at sizes small enough that no practitioner reaches them. The README’s summary is one sentence: “The result is purely asymptotic and says nothing about solving formulas in practice.”

Nobody can turn this into a runnable prediction, and that caps what the finding does for anyone shipping a solver. If you are a solver engineer choosing between a CDCL implementation and a portfolio, this paper changes nothing about your next release. It changes what you may assume about worst-case hardness.

How to Read the Claim Until Review Closes

Stefan Szeider of TU Wien told New Scientist he has looked at what was released and expects it to withstand scrutiny, but that researchers still need to check that the formally proven statement means what its authors say it means. Magnus Wahlström of Royal Holloway called the broader pattern “mathematics done by press.” Both reactions fit the evidence.

Four checks to run before you cite the result as anything:

• Read MainResults.lean and proof/PaperIndex.lean side by side. The index lists, for each numbered statement in the paper, its Lean counterpart and where the two differ. That diff is the definitional risk, stated by the authors.
• Ask whether the bound is constructive. A 2^O(…) with an uncomputed constant cannot be turned into a runnable prediction, so there is no benchmark that could confirm or kill it.
• Separate the two manuscripts. The Anthropic result and the OpenAI manuscript, dated October 17 and revised October 25, are different attacks with different write-ups and different Lean artifacts. A finding about one does not settle the other.
• Watch the panel’s published findings rather than reposts of the announcement. Tech Times reports that a public GitHub repository has been set up for independent checking, which is where a working mathematician would look first.

Where this leaves the claim: a deterministic exact counting algorithm at 2^o(n), with a kernel-checked Lean proof of the stated theorems, produced by a model in October 2026, and examined by three people with every incentive to find the hole. If it holds, a 2001 hypothesis that anchored a large share of fine-grained complexity stops being usable, and the count of results needing new foundations starts above 800. If it does not, the next thing to pin down is where the gap sat: in the algorithm, in the prose, or in the translation between them. For the earlier releases in this sequence, see our coverage of OpenAI’s 719-manuscript math release, the Navier-Stokes claim and its Lean formalization, and the release-norm debate those drops triggered.

Related Reading

More in-depth coverage from this blog on closely related topics:

• Go 1.26: runtime and toolchain changes

Sources and References

Sources cited while researching and writing this article:

• https://raw.githubusercontent.com/openai/math/main/history.md
• A $2^{o(n)}$ Time Algorithm for 3-SAT · Hexagon
• A 2^{o(n)} Time Algorithm for 3-SAT
• AI refutes 30-year-old mathematical assumption in computer science | New Scientist
• formal-math/eth at main · anthropics/formal-math · GitHub
• GitHub – leanprover/comparator · GitHub
• [2610.08144] Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
• guest post on Terence Tao’s blog
• ETH is False
• Two AI Systems Disproved Same Complexity Conjecture Independently on Same Day: 800 Papers at Risk
• Frontier AI labs say their models refuted the Exponential Time Hypothesis. What does that mean? | TechCrunch