Exponential Time Hypothesis Disproof by AI Awaits Expert Verdict

The claim that AI has disproved the Exponential Time Hypothesis is still waiting for an expert verdict, nearly two weeks after OpenAI and then Anthropic published proofs that the 27 year old conjecture is false. Both proofs have passed machine checks, but the three researchers reviewing them have not ruled, and the result changes nothing for real world software.

What is the Exponential Time Hypothesis?

The Exponential Time Hypothesis, or ETH, was proposed by Russell Impagliazzo and Ramamohan Paturi in 1999. It says that 3-SAT, a classic problem about whether a set of logical rules can all be satisfied at once, cannot be solved much faster than trying every possibility. In formal terms, the time needed has to grow exponentially with the number of variables.

Hundreds of results in theoretical computer science assume ETH is true. Many lower bounds on how fast algorithms can possibly run are built on top of it, which is why a refutation would ripple through the field.

What did OpenAI and Anthropic claim?

OpenAI's paper, bluntly titled "The Exponential Time Hypothesis is False", describes a deterministic algorithm that counts every satisfying assignment of a k-CNF formula in subexponential time while using only polynomial memory. Counting solutions is at least as hard as deciding whether one exists, so the algorithm would also break ETH's 3-SAT bound.

Anthropic posted an independent refutation of its own a day later. Both companies say the proofs were written with heavy AI involvement and checked in Lean, a program that verifies mathematical proofs line by line.

Impagliazzo, who is part of the group OpenAI asked to review the result, called it a shock. "As far as I'm concerned, this is not 100% certain," he told Science, noting that most researchers expected stricter versions of the hypothesis to fall first.

Has the ETH disproof been verified?

Partly. Volunteers have replayed both labs' Lean proofs under independent checkers. Neither lab, however, formalized the step from its own machine model to a standard one, and outside researchers closed that gap in Lean between November 2 and 5, according to a detailed status report on the refutations.

What remains is the human part. Impagliazzo, Paturi and Ryan Williams are organizing a public examination, and no verdict has been posted yet. They still need to agree that the formal definitions match the textbook version of ETH and to check the sharper bound in OpenAI's paper, which was not fully formalized.

Will this make computers faster?

No. ETH is an asymptotic statement, so a refutation only needs to win for unimaginably large inputs. Outside estimates suggest the advantage in OpenAI's checked bound only appears beyond roughly 10 to the power of 2,389 variables, far beyond any problem that could ever be stored. For anyone running SAT solvers in chip design or logistics, nothing changes.

The bigger shift is in how mathematics gets done. AI systems are now producing and machine checking results that experts considered decades away, a pattern we also saw when an AI system proved the Aaronson-Ambainis conjecture.

Why does it matter for AI labs?

For OpenAI and Anthropic, math breakthroughs have become a showcase for reasoning models and a selling point in a fierce funding race. OpenAI, for example, just closed new funding at a reported $1.25 trillion valuation, as we covered in our story on the OpenAI funding round.

If the examiners confirm the proofs, ETH would become one of the most important results ever credited to AI. If they find a gap, it will be an equally public lesson in why a machine checked proof is only as good as the statement it checks.