In October 2026 OpenAI and Anthropic each posted a Lean-checked algorithm said to break ETH. What they claim, what Lean checks, and why SAT is not suddenly easy
On 26 October 2026, OpenAI and Anthropic posted papers hours apart, each written by an AI model, each claiming that 3-SAT can be solved in 2o(n) time, which would make the Exponential Time Hypothesis false. Both came with Lean proofs. As of 1 November 2026, neither has been independently verified. This lesson is about what is claimed, what it would mean, and how to tell.
Every 3-SAT bound drawn as its exponent per variable. Pick a claimed bound and slide the hidden constant to see where it finally drops below brute force and the best known algorithm.
Each bound is drawn as its exponent per variable r, meaning a running time of 2^(r·n) up to polynomial factors. Brute force has r = 1 and PPSZ has r = 2 ln 2 − 1 ≈ 0.386. The claimed bounds have r tending to 0. The horizontal axis is log₂ n on a log scale, so it reaches n = 2^(2²⁶). The constants are not stated explicitly in the papers, so c is yours to choose; with every constant equal to 1, OpenAI’s Lean bound beats 2ⁿ only from n = 2^65,536. Move the pointer over the chart to read off values.
Both papers give a deterministic algorithm that counts the satisfying assignments of a k-CNF formula, for every fixed clause width k. Counting is at least as hard as deciding (a formula is satisfiable when its count is positive), so a fast counter is also a fast solver.
OpenAI’s manuscript, The Exponential Time Hypothesis is False (dated 25 October), states a running time of (n+m)O(1) · 2n/(log n)^(1/2+o(1)) using polynomial space; more precisely 2O(n log log n/√log n), improving to 2O(n/√log n) when the number of clauses m is at most a constant times n. Its Lean formalization proves the slightly weaker 2O(n (log log n)²/√log n). Anthropic’s paper, A 2o(n) Time Algorithm for 3-SAT, credited to Claude, gives 2O(n log log n/√log n) and formalizes that bound, and the statement that ETH is false, in Lean.
Each of these exponents is a vanishing fraction of n, so for every δ > 0 the algorithm eventually beats 2δn. That is exactly the negation of ETH. Nothing about it makes SAT fast: the rate falls to zero like 1/√log n, about as slowly as a rate can fall and still refute the hypothesis.
Ten statements from this module. Switch to “If the claims are correct” and watch them regroup: what is refuted, what loses its foundation, and what doesn’t move.
Click any card for details, then switch scenarios and click it again. Under “If the claims are correct”, red cards are refuted, amber cards lose the hypothesis they were proved from, grey cards are unaffected and green cards would become theorems. Nothing here has been confirmed: as of 1 November 2026 both claims are under review.
If ETH is false, so is the Strong ETH, and every lower bound proved from them loses its justification (see The Exponential Time Hypothesis and Fine-Grained Complexity). Some of those bounds become outright false: 3-Colouring on N vertices can be written as a 3-CNF with 3N variables, so it too would have a subexponential algorithm. Others, such as the quadratic lower bound for edit distance, were really proved from the Orthogonal Vectors hypothesis, which is not known to fall.
P versus NP is untouched. A running time of 2n/√log n is nowhere near polynomial, and while ETH implied P ≠ NP, its failure implies nothing about the converse. The theory of NP-completeness is made of theorems and stands as it was.
One consequence is positive. Since Ryan Williams’s work in 2010–11, it has been known that SAT algorithms even slightly faster than brute force can be converted into circuit lower bounds, proofs that certain functions need large circuits. OpenAI’s manuscript uses this to derive superlinear circuit lower bounds for a language in the class ENP. A faster algorithm would then be, at the same time, a new proof of hardness.
A machine-checked proof is a chain of five links. Walk along it for each claim, and read the actual Lean statements line by line.
One short file, MainResults.lean, imports only Mathlib and contains definitions only: ETH itself and the main counting theorem with the paper’s bound. Its README says plainly that no machine checks this file says what the paper says, so it is kept short enough to read.
Click the links of the chain on the left, and switch between the two claims. Only link 3 is guaranteed by a computer. Links 2 and 4 are short enough for experts to check by reading, and links 1 and 5 are where the review is happening. Statuses as of 1 November 2026, from the two public repositories and press reports.
Lean is a proof assistant: every step of a formal proof is checked by a small trusted program, the kernel. If the kernel accepts, the theorem follows from the definitions, whoever or whatever wrote the proof. That makes formalization unusually valuable for AI-generated mathematics, where nobody may yet understand the argument. But the kernel only certifies that a proof proves its statement. Whether the statement captures ETH, and whether the machine model reflects real running time, is checked by people reading short definition files, and the meaning of the result is settled by the research community.
For OpenAI’s claim, Russell Impagliazzo and Ramamohan Paturi, who proposed ETH in 1999, and Ryan Williams are leading an independent working group. They stress that their involvement is not an endorsement. Williams has said that some parts of the proof look routine but “two or three” look alien, and that if the claims hold, a decade of conditional results will need revisiting. Anthropic’s condensed account of its key idea concerns contracting tensor networks on complete graphs, recursively shrinking the exponent of the contraction cost. Whether the two algorithms are related is not yet known.
Two independent claims of the same bound, within hours, both with machine-checked proofs, is unusual evidence. It is still not peer review. This page will be updated as the review reports.
Spot a mistake or have an idea?