Unless SETH is false

“Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false).” That is the title of a 2015 paper by Arturs Backurs and Piotr Indyk, and for a decade the parenthetical sat there as fine print. On Monday, OpenAI said its models had proved the Exponential Time Hypothesis false, and with it SETH, the strong version that parenthetical names.

The claim is specific. The paper gives a deterministic algorithm that counts the satisfying assignments of any k-CNF formula in time that eventually falls below 2^(εn) for every ε, using polynomial space. It has been checked in Lean, and it is now in the hands of Russell Impagliazzo and Ramamohan Paturi, who proposed ETH, and MIT's Ryan Williams. By the paper's own accounting it refutes ETH, SETH, Gap-ETH and NSETH in one stroke.

None of that will make anything you run faster. What it retires is a warranty. ETH has been used in hundreds of papers to derive hardness results, and those results were never statements about the world. They were conditional promises (this is hard unless ETH fails), and the condition just came true. What that hands the field is an audit, not a sprint.

Start with the speed, because there isn't much. For formulas with about as many clauses as variables, the running time has the shape 2^(n/√log n), times a constant in the exponent that the paper doesn't pin down. The square root of a logarithm grows slowly enough to be a rounding error in practice: at a million variables, √ln n is about 3.7. Brute force is 2^1,000,000 steps. The new bound, before that constant, is around 2^269,000. Subexponential to a theorist. Astronomical to everyone else. And the speedup doesn't travel to other problems. The paper says so plainly:

The audit is already under way, in section 1.1.3 of the paper itself. SETH was the stated reason nobody expects a polynomial-factor improvement on quadratic time for edit distance, longest common subsequence, dynamic time warping, Fréchet distance or regular-expression matching. Some of those walls have a second footing. The bounds for longest common subsequence and regex matching also follow from the Orthogonal Vectors Conjecture, which may still hold. Fréchet distance also rests on a form of SAT hardness that lets clause width grow with n, which the new algorithm doesn't touch. A real speedup anywhere needs a reduction running the other way, from the target problem into fixed-width SAT, and the paper finds one only for Set Splitting. That is the field's next year: sorting walls into load-bearing and decorative.

The irony: the paper's cleanest new theorem is a lower bound. A 2013 result of Williams's says that if ETH is false, the class E^NP can't have linear-size circuits. Feed it the new algorithm and out comes an unconditional circuit lower bound: a language in E^NP that needs more than c·n·√log n gates. It's barely superlinear, but it's real.

A faster algorithm proved that something is hard.

One of the three shepherds is the person who built that bridge.

The skeptic's case is easy to make. Conditional results were always labeled conditional, and nobody who read “unless SETH is false” was fooled. An asymptotic bound with an unspecified constant, produced by a model, changes nothing for the engineer running a SAT solver tomorrow. All true about the solver. But the condition was never a formality. Hardness results are how a field decides where its people spend years: a graduate student told a problem is SETH-hard picks a different thesis. That allocation ran on belief in the condition, and the belief is gone.

Backurs and Indyk put the honest part in parentheses. As of Monday the parenthetical is true, and the title is a question again.