Exponential Time Hypothesis refutation: Two labs claim 3-SAT escapes exponential time

Two papers on one Monday

On Monday 26 October 2026, OpenAI added a manuscript titled "The Exponential Time Hypothesis is False" to its public mathematics repository. The repository's history file describes a deterministic algorithm that counts, exactly and in polynomial space, how many assignments satisfy a CNF formula of fixed clause width, using subexponential time, and says that its 3-SAT case refutes the Exponential Time Hypothesis, usually shortened to ETH. The commit that added it landed at 20:52 UTC. The 67-page paper is credited simply to OpenAI and dated 17 October, revised 25 October. The same release added a claimed proof bearing on the Kakeya conjectures, while a physics group led by David Gross held back a claimed quantum field theory result, The Next Web reported. This report concerns only ETH.

About six hours later, at 03:07 UTC on 27 October, which was still the evening of 26 October in California, Anthropic added a folder named eth to its formal-math repository. Its README presents "A 2^o(n) Time Algorithm for 3-SAT" by Claude (Anthropic) and says the result was discovered by an internal research Claude model, with a Lean 4 formalization written by AI models. The Anthropic paper, dated 26 October, states that the core algorithm was found on 16 October, using 14 million output tokens and no human input, that Anthropic researchers then worked with Claude on the presentation, and that an internal OpenAI model had independently and concurrently claimed a similar result. R&D World noted that both companies date the discovery to 16 October, and The Next Web reported OpenAI's account that its model found the disproof that day and checked it in Lean the next. OpenAI's repository README says the company defers entirely to the mathematical community on credit, precedence and concurrent work.

The core claim is the same in both papers. For every fixed clause width k, a deterministic algorithm counts the satisfying assignments of a k-CNF formula on n variables in time 2 raised to O(n log log n / √log n), up to a polynomial factor. Because that exponent eventually falls below every constant multiple of n, it contradicts ETH. Neither paper has been refereed, and the researchers examining the claim say in writing that their role is not certification.

A hypothesis built to organize hardness

3-SAT asks whether a formula built as an AND of clauses, each an OR of at most three variables or their negations, has an assignment that makes it true. Checking a proposed assignment is easy, while the obvious way to find one tries all 2^n settings of n variables. Since the 1980s, algorithm designers had shrunk the base of that exponential without removing it. Uwe Schöning's random walk gives about (4/3)^n, the PPSZ family pushed randomized time to about 1.308^n, and the best deterministic bound before October was about 1.328^n, figures surveyed in the related-work sections of the OpenAI paper and the Anthropic paper.

In 1999, Russell Impagliazzo and Ramamohan Paturi of UC San Diego turned that stubbornness into a working assumption. Their conference paper, Complexity of k-SAT, defined s_k as the smallest exponent rate δ for which k-SAT has a 2^(δn) algorithm, and named the hypothesis that s_3 is positive, meaning 3-SAT has no subexponential algorithm. The journal version of 2001 used the hypothesis to show that k-SAT grows strictly harder as k grows. A companion paper with Francis Zane, Which Problems Have Strongly Exponential Complexity?, supplied the tool that let the hypothesis travel. Its sparsification lemma rewrites any k-CNF formula as a disjunction of at most 2^(εn) formulas with only linearly many clauses, for any ε above zero, and its new kind of reduction showed that k-SAT, k-colorability, independent set, clique and vertex cover stand or fall together: a subexponential algorithm for any one gives one for all.

That equivalence turned ETH into a currency for hardness. Assuming it, Chen, Huang, Kanj and Xia showed in 2006 that no algorithm finds a clique of k vertices in time f(k) times n^o(k), so the brute-force approach is essentially optimal, and a long line of parameterized lower bounds took the same shape. A stronger sibling, the Strong Exponential Time Hypothesis or SETH, says the savings over 2^n vanish as clause width grows. It underwrote limits even for problems solvable in polynomial time, such as Backurs and Indyk's 2014 result that edit distance between two strings cannot be computed in strongly subquadratic time unless SETH fails. Because SETH implies ETH, a refutation of ETH refutes SETH too. The Anthropic paper reports that a literature search run by Claude found more than 800 papers proving at least one result only under ETH or a hypothesis that implies it.

The field never treated ETH as a theorem in waiting. In a 2019 essay of estimated likelihoods, Ryan Williams of MIT put ETH at 70 percent and SETH at 25 percent, urged researchers to doubt ETH a little more and to think now and then about how it might fall, and recalled Impagliazzo reminding him: "It's not a Conjecture, it's a Hypothesis!"

Two routes to one exponent

Both papers begin with the same reductions. The count-preserving form of sparsification lets each assume a formula with only linearly many clauses. Counting then becomes a sum, over all assignments, of a product of local factors, one per clause, each equal to 1 when its clause is satisfied and 0 when it is not. If the variables split into small groups with no clause straddling two groups, the sum would factor into small independent sums and the count would be cheap. Real formulas do not split that way. When the graph of clauses and shared variables is an expander, every balanced cut is crossed by a linear number of shared bits, which is why divide and conquer had only ever improved the constant in the exponent.

OpenAI's paper attacks the interactions with polynomial interpolation. It writes each clause as a polynomial, so that the clause x1 or not x2 or x3 becomes 1 minus (1 minus x1) times x2 times (1 minus x3), and the count is the sum of the product of these polynomials over all Boolean inputs. It then replaces each variable occurrence by a linear expression whose coefficients depend on an auxiliary parameter T. At T equal to zero the expression is the original variable, so the whole sum, viewed as a polynomial in T, equals the count at zero. At selected positive integers the deformed factors interact across groups only through a few shared integer linear measurements, and once those values are fixed the sum factors by group. The algorithm computes several Taylor coefficients at each such point and recovers the value at zero by Hermite interpolation. The deformations come from an auxiliary matrix built from commuting swap permutations, and parity tests drawn from expander-based Tanner codes handle formulas with many clauses. The paper's Theorem 1.1 gives the headline bound with polynomial space, and 2^O(n/√log n) when the number of clauses is at most a constant times n. Its Appendix D reaches those sharper bounds by a recursive contraction of Boolean tensor networks.

Anthropic's paper starts from the tensor-network picture. Each clause is a node, an edge carries the bits of the variables two clauses share, and the count is the contraction of that network. The key move rewrites pairs of crossing equality tests using a decomposition that the paper derives from the classical eight-square identity of Degen (1818) and Graves (1843), replacing them with signed parity functions on four nodes. The nodes are laid out on a grid, and in each term of the resulting signed sum the algorithm merges whole rows or whole columns, whichever is cheaper, which cuts the bits between nodes to at most about 11/12 of what they were. Rebalancing and recursing drives the exponent toward zero. Its main theorem gives a bound of 2^O(min{k² n log log n / √log n, km / √log m}) for m clauses. The README adds a condensed paragraph from which, it says, Claude Opus 5.5 at high effort can rederive the weaker statement that 3-SAT can be decided in time 2^(δn) for every δ above zero.

The two write-ups read very differently and were presented as independent, yet they share ingredients: sparsification, counting rather than deciding, signed cancellation in place of nonnegative counts, and algebra over swaps. Outsiders began sorting out the core within days. Shiva Kintali posted a simplified exposition of the OpenAI proof, dated 26 October, that proves only the qualitative statement for every fixed rate. Ryan O'Donnell of Carnegie Mellon posted an exposition built on sparse permanents, dated 29 October and, by its own footnote, produced through interaction with language models.

What the Lean files check, and what they cannot

Formal verification is the strongest part of this claim and the easiest part to overstate. Anthropic's folder separates the statement from the proof. MainResults.lean contains definitions only and imports nothing but Mathlib, the community library of formalized mathematics. ETHIsFalse says that for every δ above zero some deterministic machine, of Mathlib's multi-stack Turing machine kind, decides 3-SAT within a constant times 2^(δn) steps, and MainTheorem states the counting bound. The README says the proofs depend only on Lean's three standard axioms, and the folder's Comparator configuration switches on nanoda, an independently written second kernel. Comparator, a tool from the Lean project, certifies that a submitted proof states exactly what a trusted challenge file states, uses no axioms beyond those permitted, and passes the kernel. Appendix E of the Anthropic paper reports that all 1,050 Lean modules were built together from nothing.

The same appendix states the limits plainly. No machine can check that the definitions mean what the paper means; that is left to whoever reads a short file. AI models wrote the Lean development and further copies of those models reviewed it, and when the paper was written no person was known to have checked it. Its constant is not explicit. Two steps from the Lean statements to the printed theorems, encoding a formula as the machine's input word and simulating that machine on a word RAM, sit outside the formal proof. The appendix also concedes that the comparison between the Lean proof and the printed one was made by AI models rather than mechanically, and that the most exacting of them regard the formal version as a separate proof of the same theorem.

OpenAI's formalization is narrower. Its Lean scope note says Lean proves the counting bound with the weaker exponent n (log log n)² / √log n, again with polynomial space, while the sharper bound of the manuscript is proved only on paper. The challenge statement is a theorem about a counting machine's output, running time and space, and does not itself define ETH, so the deduction from it to ETH's failure is a short informal step. Its Comparator configuration leaves the nanoda option switched off. A reader comment on the reviewers' blog reports replaying both developments with Comparator and finding that each checks against its own statement. That is encouraging but is not a review.

What Lean buys, then, is strong confidence that no logical gap hides inside the formal argument. It cannot certify that the formal statement is the theorem people care about, and it supplies no understanding of why the algorithm works. Those are the tasks the review was set up to do.

Asymptotic, not practical, and not P versus NP

Anthropic's README puts it in one line: "The result is purely asymptotic and says nothing about solving formulas in practice." The paper quantifies that. For 3-CNF formulas with five clauses per variable, its proven bound does not beat the 2^n of exhaustive search until n exceeds 10^10,000, and the bound in n alone does not until n exceeds 10 raised to 10^8. The authors judge the approach unlikely to yield any general improvement below about 10^7 variables, however it is instantiated, while brute force is already hopeless at 100. Practical SAT solving, which runs on heuristics rather than worst-case guarantees, is unchanged.

Nor does the result move P versus NP. A polynomial-time algorithm for 3-SAT would refute ETH, but refuting ETH needs only something faster than every 2^(δn), and the new bound is still far from polynomial. The OpenAI paper notes that bounds of the form 2^o(n) do not survive general polynomial-time reductions, so the result does not give subexponential algorithms for NP as a whole. In his blog post of 28 October, Lance Fortnow observed that Subset Sum and the Traveling Salesman problem gain nothing, and that subexponential time for all of NP would need 3-SAT in time 2 raised to n^o(1), which this result does not approach. Williams told TechCrunch that one of his first questions to OpenAI's science lead Dan Roberts was whether any cryptosystem was affected, and that the company had checked and was reasonably confident it implied no breaks.

Some consequences follow at once if the proof holds. Through a 2013 theorem of Williams, a subexponential 3-SAT algorithm implies that the complexity class E^NP has no Boolean circuits of linear size. The Anthropic paper notes that the best previous lower bound for a language in that class over the full binary basis was 3.1n minus lower-order terms, and OpenAI derives a bound of order n√log n for infinitely many input lengths. Anthropic lists algorithms faster than 2^(δn) for every δ for independent set, clique, vertex cover and dominating set, measured by the number of vertices. Fortnow relayed Bernardo Subercaseaux's observation that nondeterministic time T can then be simulated deterministically in time about 2 raised to O(T (log log T)³ / √log T). Many fine-grained lower bounds survive on other footing. Both papers treat the Orthogonal Vectors conjecture, which SETH implies, as still standing, and the OpenAI paper points out that bounds such as the one for longest common subsequence follow from it. As Fortnow put it, the failure of ETH and SETH does not make their implications false.

Who is checking, and on what terms

OpenAI's history file says an independent working group led by Impagliazzo, Paturi and Williams will examine and explain the proof, and that the materials were made public at the group's request. The two people who proposed ETH are therefore leading the scrutiny of its claimed refutation. Their open letter is careful: "Our involvement should not be taken as certification of the claim." It asks the community how to organize an examination in which researchers contribute independently, how to make the argument accessible through simplified proofs and seminars, and how to keep established consequences apart from speculation, without giving any company or chosen group ownership of the effort. The letter then opens a second question, norms for AI-generated breakthroughs: early access, disclosure of conflicts of interest, and credit for the people who check, fix, simplify and explain results. A discussion blog hosts the effort, with a community repository and a proposed virtual meeting before the end of 2026.

The terms matter because of what came before. Williams had called OpenAI's release of hundreds of manuscripts earlier in October a "DDOS attack on mathematicians", a phrase TechCrunch recalled. This time, The Next Web reported, he said the group signed no non-disclosure agreements and is not being paid, and that OpenAI agreed to its requests to publish all raw data and to fund a research conference. To TechCrunch, Williams said that some parts of the proof looked routine but that "two or three alien-looking parts" convinced him the whole community needed to work on it, and that he did not believe OpenAI's algorithm could be the best one possible.

Fortnow, who wrote that he had not verified the proof himself, still judged in his post that "it is safe to assume now that the exponential-time hypothesis is toast." That is an informed observer's reading of two independent claims, a formal check and early expositions. It is not a refereed verdict, and as of 30 October neither paper had completed peer review.

How to place the ETH claim in AI history

Programs have proved theorems since RAND's Logic Theory Machine found proofs in symbolic logic in 1956, and language models have discovered algorithms at least since AlphaEvolve found a way to multiply 4 by 4 complex matrices with 48 scalar multiplications in 2025. In 2026 the pace changed. An OpenAI model disproved Erdős's unit distance conjecture in May, a counterexample that nine mathematicians including Gowers condensed and described as human-verified. OpenAI claimed a singularity in the Navier-Stokes equations in September, as Quanta Magazine reported, and on 6 October released hundreds of manuscripts that included a claimed quasi-Riemann hypothesis. The ETH claim sits at the end of that run, and it differs from the earlier entries in four ways.

First, the object is an algorithm, so the claim concerns computation itself, the subject from which AI grew. Second, two laboratories reached it independently, both dating the discovery to the same day. That suggests the idea lay within reach of current frontier models rather than being a one-off, although it also means two companies with commercial reasons to claim priority released in the same evening. Third, the formal check covers the headline statement itself, in one case with a second kernel, rather than a fraction of a larger catalogue. Fourth, the hypothesis's own authors are running a public review that asks, alongside correctness, who should get credit when machines find results first.

The limits are just as specific. There is no refereed version. The Lean statements were checked against the papers by models, not yet by named human experts, and human understanding is still being assembled through expositions, one of them produced with language models. The algorithm has no practical use. The record therefore treats this event as Provisional. If the proof survives review, machine-made mathematics will have overturned a hypothesis that hundreds of papers built on. If it fails, the lesson will lie in where: the mathematics, the gap between a formal statement and its meaning, or the speed at which a field was asked to absorb it.

References

• OpenAI (2026). openai/math history: October 26, 2026.
• OpenAI (2026). Update math/cs papers, formalizations, and verification data, commit 42907c9.
• OpenAI (2026). The Exponential Time Hypothesis is False.
• OpenAI (2026). openai/math: manuscripts and proof artifacts from an internal OpenAI model.
• OpenAI (2026). Lean scope note: The Exponential Time Hypothesis is False.
• OpenAI (2026). SubexponentialSAT Comparator challenge statement.
• OpenAI (2026). SubexponentialSAT Comparator configuration.
• OpenAI (2026). The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re s > 7/8.
• Anthropic (2026). Add eth: paper and Lean 4 formalization, commit 16a5ce4.
• Anthropic (2026). eth: A 2^o(n) Time Algorithm for 3-SAT, README.
• Claude, Anthropic (2026). A 2^o(n) Time Algorithm for 3-SAT.
• Anthropic (2026). MainResults.lean: the two main results as Lean statements.
• Anthropic (2026). eth Comparator configuration.
• leanprover (2025). Comparator: a trustworthy judge for Lean proofs.
• Impagliazzo and Paturi (1999). Complexity of k-SAT.
• Impagliazzo and Paturi (2001). On the Complexity of k-SAT.
• Impagliazzo, Paturi and Zane (2001). Which Problems Have Strongly Exponential Complexity?.
• Chen, Huang, Kanj and Xia (2006). Strong computational lower bounds via parameterized complexity.
• Backurs and Indyk (2014). Edit Distance Cannot Be Computed in Strongly Subquadratic Time, unless SETH is false.
• Williams (2019). Some Estimated Likelihoods for Computational Complexity.
• Impagliazzo, Paturi and Williams (2026). Letter to colleagues on the claimed refutation of ETH.
• ETH: Community Examination and Discussion (2026). ETH refutation: examination and discussion.
• Fortnow, Computational Complexity blog (2026). The Exponential-Time Refutation.
• Kintali (2026). A simplified proof of ETH is false.
• O'Donnell (2026). Some exposition of The Exponential Time Hypothesis Is False.
• Ana Maria Constantin, The Next Web (2026). OpenAI says its AI model has disproved the Exponential Time Hypothesis.
• Tim Fernholz, TechCrunch (2026). Frontier AI labs say their models refuted the Exponential Time Hypothesis. What does that mean?.
• Brian Buntz, R&D World (2026). OpenAI says its AI models produced major proofs in mathematics, computer science and physics.
• RAND Corporation (1956). The Logic Theory Machine: A Complex Information Processing System.
• Google DeepMind (2025). AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms.
• Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood (2026). Remarks on the disproof of the unit distance conjecture.
• Konstantin Kakaes, Quanta Magazine (2026). AI Has Solved One of Math's $1 Million Millennium Prize Problems.