Two artificial intelligence labs say their models have refuted the Exponential Time Hypothesis, one of the standard assumptions of computer science, and both date the discovery to the same day. OpenAI said on 26 October that an internal model found a disproof on 16 October and that it was checked in the Lean proof language the next day, in a post on its website. Hours later Anthropic published its own paper, saying an internal Claude model found a similar algorithm on 16 October, “with 14M output tokens and no human input”.
Neither claim has yet been confirmed by independent experts. Both companies say the result is theoretical: it does not make any real-world problem faster to solve today. Here is what the hypothesis says, what the two labs claim, and why investors in AI have reason to care anyway.
What is the Exponential Time Hypothesis?
The Exponential Time Hypothesis, or ETH, is a claim about how hard a classic puzzle is. In the puzzle, called 3-SAT, a computer gets a long list of rules, each linking up to three yes-or-no switches, and must find a setting of the switches that satisfies every rule. Checking an answer is easy. Finding one, as far as anyone knew, is not: with n switches, trying every setting takes 2ⁿ steps, and that number doubles with each switch added.
Researchers have long shaved the problem down. The best deterministic method before this month took about 1.328ⁿ steps, Anthropic’s paper notes. That is far faster than 2ⁿ, but it still grows exponentially. ETH, set out by Russell Impagliazzo and Ramamohan Paturi in a 2001 paper, says it always will: that no algorithm can solve 3-SAT in time that grows more slowly than some exponential.
ETH is stronger than the famous assumption that P does not equal NP. Researchers use it as a building block: if ETH is true, they can prove that hundreds of other problems also need exponential time. Anthropic’s paper says a literature search found more than 800 papers that prove at least one result only under ETH or a stronger hypothesis that implies it.
What OpenAI and Anthropic say their models proved
Both claim an algorithm that solves 3-SAT in what mathematicians call 2^o(n) time: slower than any polynomial, but faster than every exponential once the problem is large enough. That is enough to refute ETH.
- OpenAI says its system “recently proved that the ETH is false”, and that the result was then verified in Lean, a language in which computers check every step of a proof. It has handed the work to a group led by Mr Impagliazzo and Mr Paturi, both of UC San Diego, and Ryan Williams of MIT. It has also agreed to fund a conference on what the result means.
- Anthropic’s paper describes a deterministic algorithm that also counts every solution, a harder task. Its proof is formalised in Lean 4 and public on GitHub. The paper says Anthropic researchers worked with Claude to improve the presentation, and it notes that an OpenAI model “claims to have proven a similar result” at the same time.
A machine-checked proof is strong evidence, but it is not the end of the review. Anthropic’s paper says its Lean development “was written by AI models and reviewed by other instances of the same models”, and that at the time of writing no person is known to have checked it. Lean confirms that the proof follows; people still have to confirm that the statements say what the paper claims. That is the job of the expert group, and of the wider field over the coming months.
OpenAI announced two other results in the same post: a proof of the local smoothing conjecture in harmonic analysis, which it says also resolves the Kakeya conjecture in all dimensions, and an existence proof for quantum chromodynamics. The physics group, led by the Nobel laureate David Gross, has chosen not to release the AI-produced material yet.
Does refuting the Exponential Time Hypothesis break encryption?
Not on the companies’ own reading. Anthropic’s paper says the result “does not bear on the P vs NP question directly, nor does it yield any practical algorithms” for the hardest class of problems. For formulas with five rules per switch, its bound beats trying every setting only above 10^10,000 switches. Trying every setting is already impractical at about 100 variables, the paper notes. OpenAI says turning the theory into practical improvements “will require significant further research”.
Claims on social media that the result explains a wave of AI-found software flaws go beyond what either company says. Those flaws, such as the PHP vulnerability we covered on 22 October, come from models reading code, not from a new algorithm for 3-SAT.
Why markets should still pay attention
What changed is less the mathematics than who did it. Two labs say their models found, within hours of each other, a counter-example to an assumption the field had relied on for a quarter of a century. That is a claim about capability, and capability is what investors are paying for.
The timing is not lost on them either. Anthropic’s filing to list its shares became public on 26 October, the same day as both announcements, as we reported yesterday. The race is costly: we wrote last week on Anthropic’s plans for computing power.
If the proofs hold, they support the case that frontier models can now do original research, not only summarise it. If the experts find a gap, the episode will show how far machine checking can be trusted when no human has read the proof.
What to watch
- The review by the Impagliazzo, Paturi and Williams group, and any response from other complexity theorists to the two papers.
- Whether the two algorithms are the same idea. Each lab found its result on 16 October; a side-by-side reading will show whether they took one route or two.
- Anthropic’s listing timetable, and how both labs present research results to investors.