If ETH is false, what changes for software

Article

Artificial Intelligence

Local AI with open-weight models, agentic AI with human approval and governed AI, on-premise or in a private cloud.

Discover →

Cybersecurity

CISO-as-a-service consulting: posture, remediation roadmap, ongoing support.

Discover →

Yesterday OpenAI announced three results produced by its internal models. One of them directly concerns anyone who works with software: an algorithm that, if the ongoing verification confirms it, refutes the Exponential Time Hypothesis (ETH). Formulated between 1999 and 2001 by Russell Impagliazzo, Ramamohan Paturi and Francis Zane, it states that the 3-SAT problem requires, in the worst case, time truly exponential in the number of variables. Stefano Noferi wrote about it this morning in The exponentials we cannot see. His thesis is summarised at the end.

Here we look at the possible concrete consequences: SAT solvers, counting solutions, algorithms that for ten years were considered optimal, cryptography. One caveat applies to everything that follows. The result is formalized in Lean, but the external group’s verification and reading have only just begun, so all of this should be read in the conditional.

The result in brief

SAT (satisfiability) is the reference problem of theoretical computer science. Given n variables that are true or false and a formula combining them with “and”, “or” and “not”, for example (x₁ or not x₂) and (x₂ or x₃), the question is whether some assignment makes the formula true. Checking a proposed solution is immediate; finding one may mean trying 2ⁿ combinations. In k-SAT the formula is a list of conditions, the clauses, each with at most k variables (a k-CNF formula). With k = 3 the problem is NP-complete: every problem in the class NP can be translated into it.

ETH says that for 3-SAT there is nothing substantially better than exponential time, that is 2^cn for some constant c. Its strong version, SETH (Strong ETH), says that as clauses get longer one cannot do much better than exhaustive search, 2ⁿ. Neither has ever been proven, but for twenty-five years both have been used as if they were true.

The paper presents a deterministic algorithm that, for every fixed k, counts the satisfying assignments of a k-CNF formula with n variables and m clauses in time (n+m)^O(1) · 2^{O(n log log n / √log n)}, using a polynomial amount of memory. When the number of clauses grows at most linearly with the variables, the time drops to 2^{O(n / √log n)}. This is subexponential time: it grows more slowly than any 2^cn, although it still grows faster than any polynomial. If the theorem stands, ETH and SETH fall and, according to the paper, so do several variants of the two hypotheses.

A comparison with the state of the art gives a sense of the jump. For 3-SAT the best randomized bound cited in the paper is about 1.307ⁿ and the best deterministic one about 1.328ⁿ. For counting the solutions of 3-SAT the best deterministic bound was about 1.637ⁿ.

The paper is also explicit about what the result does not say:

• the running time is still superpolynomial, so P versus NP remains open;
• subexponential time for SAT does not transfer through general translations between problems, so subexponential algorithms for all NP problems do not follow;
• the constants hidden in the O notation depend on k and are not quantified. The paper contains no implementation and no measurements.

OpenAI writes that turning the theoretical advance into practical improvements will require significant further research.

SAT and SMT solvers: no immediate effect

SAT solvers, and SMT solvers that extend SAT with arithmetic, arrays and other theories, are everyday infrastructure: formal hardware verification, test generation, static analysis, planning, dependency resolution in package managers. Their real-world performance depends on the structure of industrial instances, exploited by techniques such as clause learning and variable selection heuristics. The theoretical worst case matters little in daily use.

A better asymptotic bound, with unknown constants and no implementation, does not make any solver installed today faster. The open question is the technique, which is algebraic and different from the local search and branching of current solvers: the formula becomes a polynomial, variables are grouped, and counting is reduced to counting the common zeros of sparse polynomial systems. Whether any of these ideas translate into preprocessing or new search strategies will only become clear when someone tries to implement them.

Counting solutions

The point technically closest to practical use is that the algorithm counts. Model counting (#SAT) is used in probabilistic inference, quantitative verification (how many inputs lead to a given state), configuration space analysis and system reliability. It is harder than deciding satisfiability, and the exact counters in use today hold up on well-structured instances.

From counting, the paper also derives exactly uniform sampling of a solution, which is what constrained random test generation needs. It also obtains subexponential algorithms for counting independent sets, colourings and perfect matchings of a graph, and, in subexponential time, arbitrarily accurate approximations of Max-k-SAT, the variant that seeks to satisfy as many clauses as possible. These remain worst-case results: they are worth watching, without expecting new tools soon.

SETH-based lower bounds

This is where the consequence is most concrete, even if for now it concerns arguments more than code. Over the last ten years SETH has been the basis for a series of results of the form “this quadratic algorithm cannot be improved substantially, unless SETH is false”. The paper lists them:

• edit distance, which underlies diff tools, spell checkers and sequence alignment;
• longest common subsequence and dynamic time warping, used in bioinformatics and time series;
• Fréchet distance, for comparing trajectories;
• regular expression matching;
• approximate graph diameter, reachability under updates, problems parameterized by treewidth, which measures how closely a graph resembles a tree.

These bounds have guided design choices: for exact edit distance on long strings the recommended route was approximation or heuristics, because an exact algorithm much faster than quadratic would have refuted SETH.

The paper says the refutation removes one basis for these claims. It also points out that several of them follow from weaker hypotheses that may still hold. LCS and regular expressions, for example, also follow from the Orthogonal Vectors Conjecture (OVC), which states that finding two orthogonal vectors across two sets of binary vectors takes essentially quadratic time. SETH implies OVC; the converse is not known. Fréchet distance, diameter and treewidth also follow from the analogous hypothesis for SAT with clauses of unbounded length, while the new algorithm holds for fixed k.

To obtain a faster algorithm for a specific problem, a reduction in the opposite direction is also needed, from the problem to SAT with fixed-length clauses, keeping the number of variables under control. The paper gives one only for Set Splitting with sets of bounded size, which becomes subexponential.

In practice no diff tool or aligner gets faster tomorrow. What changes is the status of some sentences found in documentation, papers and design discussions: “it is proven that we cannot do better” becomes, for part of these problems, an open question again. The paper itself speaks of a renewed search for algorithms.

Cryptography

The paper does not address cryptography in use. RSA, elliptic curves, AES and lattice-based post-quantum schemes rest on specific problems, and their security estimates come from the best known attacks on those problems: the paper proposes no new ones.

The only passage close to cryptography is in an appendix and concerns local one-way functions. A one-way function is easy to compute and hard to invert; in local ones each output bit depends on a constant number of input bits. The paper shows that constant-locality versions of the candidate functions proposed by Oded Goldreich in 2000 can be inverted in 2^o(n) time, so they do not have exponential inversion hardness. It adds that this does not rule out that they remain one-way against polynomial-time algorithms. These constructions are studied mainly in theory, for example for local pseudorandom generators: anyone using them as an assumption will need to revisit the parameters.

Verification

The AI produced the refutation on 16 October and the formalization on 17 October in Lean, a language in which a program mechanically checks every step of a proof. The repository contains the paper and the Lean proof. The formalized version covers a slightly weaker bound, with exponent n (log log n)² / √log n, which is still enough to refute ETH.

Verifying and explaining the result has been entrusted to an external group led by Impagliazzo, Paturi and Ryan Williams. The group asked for all raw data to be made public and for OpenAI to fund a conference on the consequences for the field. OpenAI agreed.

It is the same pattern we saw with Navier-Stokes: an artefact that can be checked mechanically, without having to trust whoever produced it. For teams working with agents in research and development the lesson remains practical: tests, types and verifiers written before generation is scaled up.

What to watch

• The outcome of the verification by Impagliazzo, Paturi and Williams, and the conference on the consequences.
• The first implementations and measurements, which will show how much the constants weigh for small k.
• New algorithms for problems whose hardness rested only on SETH, and translations to SAT with fixed-length clauses.
• Any effects on model counters and constrained random test generators.

Stefano Noferi’s thesis

In his article Noferi reads the result as one case of a more general difficulty: people struggle to grasp exponential phenomena. It applies to the growth of AI, where according to METR the length of tasks models complete on their own doubles roughly every seven months: if the trend continued, five years would mean eight and a half doublings, a factor of almost 400. It applies to pandemics and to viral phenomena. It applies to ETH, where, if the result stands, for more than twenty-five years the boundary between exponential and subexponential had been placed in the wrong spot.

The difficulty has been measured: Wagenaar and Sagaria in 1975, Lammers, Crusius and Gast in 2020 on infections, Dehaene on our spontaneous intuition of numbers, which is logarithmic.

Noferi adds an order of magnitude that also matters to anyone who writes software. As a rough indication, with base-2 logarithms, ignoring constants and using the general bound, for a formula with a million variables the exponent of the new algorithm is still about n, the same as exhaustive search. Halving it takes about 10⁷⁷ variables, close to the number of atoms in the observable universe. Exponential and subexponential part ways at scales no direct experience reaches.

And yet we are the product of phases of very fast growth, such as the Cambrian explosion and the other evolutionary radiations. Eldredge and Gould’s theory of punctuated equilibria, still debated, describes evolution as long periods of stability interrupted by brief accelerations. These happen over millions of years, though, while our intuition is calibrated on the span of a life, and often on just a few days. That is why we need tools that extend it. Repeated measurements like METR’s make growth visible before it becomes obvious. A proof in Lean lets us verify that a subexponential algorithm exists even when intuition does not see it. For Noferi this is the role of the human part in a governed superintelligence: deciding what matters, verifying and answering for the results.

Sources

• OpenAI, Working with academic communities to build scientific understanding (26 October 2026)
• OpenAI, The Exponential Time Hypothesis is False, paper revised on 25 October 2026 (PDF)
• OpenAI, scope of the Lean formalization
• Impagliazzo and Paturi, On the complexity of k-SAT (2001)
• Backurs and Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false)
• Goldreich, Candidate One-Way Functions Based on Expander Graphs (ECCC, 2000)
• Stefano Noferi, The exponentials we cannot see
• Navier-Stokes and augmented intellectual work