Exponential time hypothesis disproved by an OpenAI model?

On October 26, OpenAI published the paper “The Exponential Time Hypothesis is False” in its openai/math repository. According to the paper, an undisclosed internal OpenAI model has disproved the exponential time hypothesis (ETH), one of the basic assumptions of computational complexity theory. An independent group of computer scientists, including two co-authors of the hypothesis itself, is examining the paper together with its Lean formalization.

What is the exponential time hypothesis?

ETH (Exponential Time Hypothesis) assumes that 3-SAT, the problem of checking whether a logical formula with three-variable clauses can be satisfied, cannot be decided faster than in 2^Ω(n) time for n variables. Put simply: with every extra variable the time grows exponentially, and no clever algorithm will change that.

The hypothesis was formulated by Russell Impagliazzo and Ramamohan Paturi (with Francis Zane). Hundreds of papers rest on ETH, proving that some problem in graphs, databases or computational biology “cannot” be solved faster (as The Next Web points out).

What exactly did the OpenAI model prove?

The paper gives a deterministic algorithm that exactly counts all satisfying assignments of a k-CNF formula for every fixed k ≥ 2. It runs in polynomial space and in time (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), i.e. subexponential. The 3-SAT case is enough to refute ETH.

Interestingly, the algorithm doesn’t just answer “yes” or “no”, it counts the solutions. From this, the paper derives further results:

1. subexponential algorithms for counting graph colorings, independent sets and perfect matchings,
2. arbitrarily accurate approximations for Max-k-SAT in subexponential time,
3. a new lower bound on the size of logic circuits for the class E^NP.

According to The Next Web, the model found the proof on October 16, and a day later it had already been verified in Lean (a formal language for computer-checked proofs). In the repository changelog, OpenAI states that the paper went online together with its Lean formalization.

Who is checking the proof?

The group that is to examine and explain the proof is led by Russell Impagliazzo, Ramamohan Paturi (UC San Diego) and Ryan Williams (MIT). According to the repository changelog, it was at this group’s request that the materials were published right away, so that everyone could check them. Williams wrote on X that an internal OpenAI model had produced a “claimed refutation of ETH”, i.e. a claimed disproof of ETH.

The researchers haven’t signed any NDAs and aren’t being paid for this (according to The Next Web). They asked OpenAI to release all the raw data and to fund a conference on the consequences of the result, and the company agreed. In an open letter, however, they stress that their involvement is not a confirmation of the result (“should not be taken as certification of the claim”), adding that if the proof is correct, “it will change an important part of theoretical computer science”.

Is this something new in the AI world?

This isn’t OpenAI’s first such publication. As we know, on October 6 the company put more than 700 model-generated math papers into the same repository. The repository README says the model was given about 4,000 open problems, and each result took on average three hours of “thinking” at the ChatGPT Pro level.

What’s new is that on October 26 OpenAI announced three results at once and chose a different path for each (as Unite.AI describes):

1. ETH: the paper and the Lean proof are public, and an open group of Impagliazzo, Paturi and Williams is checking them.
2. Sogge’s “local smoothing” conjecture in all dimensions, which according to OpenAI implies the Kakeya conjecture and Stein’s restriction conjecture: also published with a Lean proof.
3. The existence of Yang-Mills theory and QCD in four dimensions (one of the Clay Institute’s Millennium Problems): no materials yet. A group led by Nobel laureate David Gross decided to write up the result itself.

OpenAI also declares that it doesn’t want scientific credit for its models’ discoveries. The credit is to go to the people who understand and describe them. The company has also given $5 million to the Simons Foundation for workshops and conferences on AI-generated results.

What should we watch out for?

First, the state of verification. A Lean formalization is a strong signal, but you always have to check whether the theorem stated in Lean really says the same thing as the paper’s text. OpenAI itself writes in the README that some results without formalization may contain errors, and on October 7 it withdrew three papers because of a sign error in one of the proofs. So let’s treat the result with caution until the group finishes its work.

Second, what the result does not mean. The authors state plainly that it does not follow that all NP problems have subexponential algorithms. So this is not a resolution of P vs NP, and the running time still grows faster than any polynomial.

Third, the pace. A result theorists had worked on for more than 20 years was reportedly found by the model as part of an internal evaluation. If it holds up, it will probably be the strongest example yet of AI making independent discoveries in theoretical computer science. It also brings back the topic of formal proofs, which I wrote about in the post on formal verification with Claude.

FAQ

What is the exponential time hypothesis?

It’s the assumption in complexity theory that 3-SAT cannot be solved in less than 2^Ω(n) time for n variables. It was formulated by Impagliazzo and Paturi with Francis Zane.

Has OpenAI solved P vs NP?

No. The algorithm is subexponential but not polynomial, and the authors point out that the result does not carry over to all NP problems.

Is the disproof of ETH already confirmed?

Not yet. There is a Lean formalization, but the independent group of Impagliazzo, Paturi and Williams is only now examining it and stresses that its involvement does not mean confirmation.

Which OpenAI model did this?

An undisclosed internal model. OpenAI doesn’t give its name in the repository README.