For thirty years, the Exponential Time Hypothesis has been one of those assumptions that quietly holds up a wing of computer science. It says 3-SAT cannot be solved in subexponential time. If true, it implies P ≠ NP. It is also the foundation for a whole genre of "fine-grained" lower bounds: proofs that a problem can't be solved much faster than the obvious algorithm, conditional on ETH.
This week, two labs published proofs that it is false. Anthropic put one out. OpenAI put out another. Then Shiva Kintali posted a simplified exposition that walks through OpenAI's argument using sparsification, bounded occurrences, spectral replacement, and rational interpolation, giving a deterministic 3-SAT algorithm that runs in time roughly 2^(εn) for any fixed ε > 0.
If that holds, ETH is dead. And P versus NP is still open.
What actually changed
The distinction matters more than the headline. ETH being false means 3-SAT is subexponential — faster than 2^n by an unbounded factor as n grows — not that it is polynomial. The problem remains NP-complete, and nobody has a polynomial algorithm. What breaks is the conditional infrastructure: results of the form "if ETH holds, then this problem requires n^(2−δ) time" lose their premise. The edifice doesn't collapse; it becomes unmoored.
That's the part practitioners will feel. Fine-grained complexity gave us a vocabulary for why some quadratic algorithms are probably optimal. If ETH falls, a lot of those "probably" statements revert to "unknown" — not false, just no longer supported.
The interesting part is the verification
Mathematical results usually arrive as a paper, then a seminar, then a slow accretion of citations and re-derivations. This arrived as two industrial labs publishing within days of each other, followed almost immediately by a third party simplifying the argument.
That's not a scandal. Kintali's simplification is exactly what you want: an independent reader turning a dense proof into something teachable, and in the process checking it. But it also shows where the bottleneck has moved. Generating a candidate proof is now cheap enough that two organizations did it in parallel. Digesting one is still expensive.
There is a second signal worth noting. John D. Cook's post mentions a comment he saw elsewhere: the statement formalized in Lean was slightly weaker than the statement the paper claims. The subexponential result still holds, but "slightly weaker" is doing real work in that sentence. A machine-checked proof guarantees that some theorem is true; it does not guarantee it is the theorem in the abstract. That gap is where errors and overclaims live, and it is invisible to anyone who reads "formally verified" and stops.
The commenter asking whether the proofs are "code slop" is asking the right question badly. The question isn't whether a machine wrote it. It's whether anyone has checked that the formal statement matches the natural-language claim, and whether the constants survive scrutiny.
What a good response looks like
Not deference, and not dismissal.
Deference would be treating "Anthropic and OpenAI both published" as verification. Two labs can make the same mistake, especially if they share methods or training data, and simultaneity is weak evidence of correctness.
Dismissal would be treating fast, machine-assisted proofs as slop by definition. The Monien–Speckenmeyer algorithm from 1985 is still the reference point here; the new algorithm is a different kind of object, and if it checks out it is simply better.
The reasonable response is procedural: read the simplified proof, verify the formal statement, check the constants, and wait for the part that always takes time — other people using the result. A theorem becomes real when strangers build on it and nothing breaks.
Why this one is worth watching
Complexity theory has spent decades as a field where progress is measured in decades. A result that moves a load-bearing assumption is rare enough that the surrounding sociology is worth studying too. We just watched a claim go from preprint to simplification in about a day, with formal verification in the loop and a caveat about the formalized statement surfaced in a blog comment.
That is a faster and more transparent process than the field is used to. It is also easier to fool. The two failure modes are symmetrical: a community that only trusts slow human proofs will ignore real results, and a community that treats Lean output as a certificate will accept weaker theorems than the ones being advertised.
The proof is not the result. The result is what survives everyone else's attempts to use it. We are about to find out, in public, at unusual speed.
Source: The Exponential Time Hypothesis is False — John D. Cook.