ETH refutations, twelve days on: both Lean proofs reach a standard Turing machine, the examiners haven't ruled, and the algorithms are brute force below 2^131,071

Twelve days after OpenAI said one of its models had refuted the Exponential Time Hypothesis, and eleven after Anthropic posted an independent refutation of its own, nobody with standing has said the hypothesis is dead. Nobody has said it survives either. What has changed is how much of the question a machine can now answer. Volunteers have replayed both labs' Lean proofs under two independent kernels, and by November 5 both labs' formal statements had been carried, in Lean, down to an ordinary multitape Turing machine reading a binary encoding of the formula. The examiners Russell Impagliazzo, Ramamohan Paturi and Ryan Williams have not posted a verdict. And two outside calculations, one of which we reran, put numbers on something the papers only say in words: both algorithms are exhaustive search on every input that could ever be written down.

We covered OpenAI's claim on October 26. This is what the examination looks like now.

Two claims, not one

The day after OpenAI's release, Anthropic published A 2^o(n) Time Algorithm for 3-SAT, credited to "Claude (Anthropic)" and found, its repository says, by "an internal research Claude model". It is a different algorithm: a recursion on tensor networks over a complete graph, where the nodes are laid out on a grid, the crossing diagonals of each rectangle are rewritten as a signed sum of cheap pieces, and rows or columns are merged term by term. It counts satisfying assignments of 3-CNF formulas in 2^O(n log log n / √log n) time, the same shape of bound as OpenAI's, with its own Lean 4 development. The README is blunter than either lab's announcement: "The result is purely asymptotic and says nothing about solving formulas in practice."

That second claim matters for verification. If two unrelated proofs reach the same conclusion, a subtle definitional slip in one of them becomes less likely to be the whole story, and the Lean work below now connects the two.

What the machines have checked

There are three separate questions here, and they keep getting blurred in coverage: does each proof check against its own formal statement, does that formal statement say what complexity theorists mean by ETH, and is the paper's sharper natural-language bound right.

The first question is now answered several times over. On the organizers' discussion blog, Totó Busnello reported on October 31 that both developments pass Lean's Comparator with only the three standard axioms. The two runs were not equally strong. OpenAI's challenge file sets enable_nanoda to false, so its proof was checked by Lean's default kernel alone; Anthropic's configuration turns on nanoda, an independently written kernel, and both kernels accepted it. The costs differ too: 3 h 47 min over 12,014 build jobs for OpenAI's development, 42 minutes on five cores for Anthropic's. Carlos Toledo replayed both with Comparator, Lean's kernel, nanoda and leanchecker --fresh, and on November 5 Nathaniel Jose reported a clean replay of both on macOS.

The second question is where the real progress of the past week sits. Neither lab formalized the step from its own machine model to a standard one. OpenAI's statement uses a primitive multi-tape machine of its own design. Anthropic's is stated on Mathlib's Turing machines, with n written in unary and the clauses in binary, and its own file says the step to a standard machine model is "not part of the Lean statements or proofs". Over November 2–5 that gap was closed in Lean by outsiders. Daniel Hawkley published a Lean 4 bridge from a positive-rate formulation of ETH to Anthropic's MainResults.ETHIsFalse. Toledo then proved in Lean that Anthropic's ETHIsFalse yields a subexponential 3-SAT decider on cslib's multitape Turing machine with a binary encoding, and on November 5 ported both labs' developments into a single Lean setup, leaving 762 of 809 and 3,190 of 3,210 files unchanged, so that both reach the negation of ETH stated for that standard machine.

Toledo is careful about what that buys. Whether complexitylib's ETH on cslib's machine "is the textbook ETH is a reading of a definition", and that cannot be delegated to a kernel. He also discloses that Claude wrote the bridge proofs and his checking tools, so "this is not an independent second party", and that on OpenAI's 2.45 GB proof export four of the six checkers he tried hit resource limits. One more irony is worth stating plainly: much of the checking of an AI-generated proof, including Anthropic's, has been done with tools that Anthropic's own model helped write.

The third question has no public answer. OpenAI's Lean theorem proves a weaker exponent, n(log log n)²/√log n, than the paper's n log log n/√log n, which rests on the prose proof alone. We found no published expert reading of it.

What the examiners have said

Very little, and on purpose. The organizers' opening post says "our involvement should not be taken as certification of the claim". Since then the ethdiscussion.blog has added a links page, the Lean replication thread and, on November 1, a call for "New Results Related to ETH". No findings on either claim have been posted there. On X, Williams's November 1 post on the subject pointed readers to that thread and to a spreadsheet of consequences. A virtual meeting before the end of 2026 is still only proposed.

Human understanding is moving faster than certification. On November 5 Ryan O'Donnell of Carnegie Mellon said he had finished teaching the proof in his graduate complexity class:

It "can be done just using classical complexity theory ingredients", in his words. That is not a referee report, but a proof that fits into a few lectures of a standard course is a proof many more people can now attack.

Brute force below 2^131,071

Both papers say their algorithms are not meant to be run. Two outside calculations say how far from runnable they are.

Stefan Szeider of TU Wien read the parameter choices of OpenAI's paper. The main construction sets λ = ⌈log2 n⌉, ν = ⌈log2 λ⌉, r = ⌊√λ/ν²⌋, Q = ⌊λ/(128ν)⌋ and R = 4⌈√λ⌉ (equation 2.19), and the paper says that if any of its numerical checks fails, "the algorithm abandons the branched computation and checks the original equations directly on all 2^n assignments". Appendix D, which carries the sharper main theorem, uses u = ⌊ελ/2^d⌋ with ε = 1/(128 · 1024) and λ = ⌈log2(n+m)⌉, and handles smaller sizes "by direct summation". So the root call needs λ ≥ 131,072.

We downloaded Szeider's script, checked its formulas against those passages of the 67-page paper, and ran it. It reproduces his numbers exactly: the three checks of the main construction first pass together at λ = 10,909,384,704, meaning the algorithm is exhaustive search for every formula with fewer than 2^10,909,384,703 variables, and the Appendix D algorithm for every input with n + m below 2^131,071. A small oddity falls out of the same run: the check 6R ≤ Q is not monotone. It passes at that λ, then fails again for the next 104,447 values, because ⌈√λ⌉ ticks up before ⌊λ/(128ν)⌋ catches up.

For Anthropic's algorithm, Ruhollah Majdoddin's arXiv paper Lowered crossover points of Anthropic's subexponential 3-SAT algorithm asks the harder question: not when the algorithm stops being brute force, but when its proven bound beats the best known algorithms. For #3-SAT with as many clauses as variables, the recursion as written wins only beyond about 2^33,858 clauses. With a series of changes he proves, that falls to about 2^420, which is still roughly 10^126 clauses. For general 3-SAT his estimate drops from 2^(2.2·10^12) to 2^(8.6·10^9) variables, and he estimates OpenAI's Appendix D route at about 2^(4.4·10^10) clauses at density one.

The more interesting part is a lower bound. Majdoddin defines a class of "rewrite-and-merge" algorithms that contains Anthropic's recursion, and shows that no grid algorithm in it can gain on general 3-SAT below about 2^6000 variables. If that holds, better bookkeeping will not make these methods practical; something with a genuinely different structure would be needed. Majdoddin discloses that the paper was written with Claude Opus 5.5 and Claude Fable 5.1 under his direction.

None of this bears on whether ETH is false. A 2^o(n) algorithm refutes an asymptotic statement however late its advantage appears, as we noted in our first post when we estimated that the exponent in OpenAI's Lean bound only drops below n beyond about 10^2,389 variables. It does settle the practical question for anyone who runs SAT solvers: nothing changes.

The consequences are arriving first

While the main claims wait for a reading, results that assume them are piling up. The organizers' November 1 thread has 21 comments. Among them: Subercaseaux and Strassle on NTIME(t) ⊆ DTIME(2^o(t)); Gheorghiu (IBM) and Aparna Gupte (MIT) on subexponential classical sampling from quasilinear-size quantum circuits; Chukhin of JetBrains Research on circuit depth reduction; Charlie Cruz on NTIME(n) ⊊ DSPACE(n); and Gupte's spreadsheet of cryptographic consequences, the one Williams pointed to. Siyuan Zhuang posted simplified versions of the Lean proofs. Majdoddin observes that either refutation also kills the Sparse Max-3-SAT Hypothesis of Alman and Vassilevska Williams, though neither paper says so.

Szeider went the other way, asking what survives. In a note on Zenodo he proposes a k×k Clique Hypothesis and finds that 20 of 29 ETH-based lower bounds from Cygan et al.'s parameterized algorithms textbook still follow from it verbatim, and the other 9 in weaker form. For the many papers whose hardness results were conditioned on ETH, that is the more useful kind of follow-up.

Several were produced with AI assistance, and at least one, Yann Tal's note on modular factorials, is labeled as AI-generated and unedited. They all stand on the two refutations as black boxes. If one of those boxes turns out to be wrong, the cleanup will be large.

Where this leaves it

The machine-checkable parts of the ETH question have been done, redone and connected across labs in under two weeks, mostly by volunteers, mostly with AI help. What remains is the part that was always going to need people: agreeing that a formal definition is the textbook one, reading the sharper bound in OpenAI's prose, and the examiners saying what they found. Until then, "Lean-verified" is accurate for both claims and "ETH is false" is still a claim, an unusually well-supported one.