OpenAI and Anthropic each say an internal AI model has disproved the Exponential Time Hypothesis, a conjecture computer scientists have used as a working assumption for more than two decades. Both companies released papers and proofs formalized in Lean, software that checks mathematical proofs step by step. The researchers organizing outside review of OpenAI’s claim say they have not certified it.

The hypothesis, first published by Russell Impagliazzo and Ramamohan Paturi in 1999, holds that 3-SAT, the problem of deciding whether a logical formula can be satisfied, requires time that grows exponentially with the number of variables. It is a stronger claim than the widely held belief that P does not equal NP. Anthropic’s paper says a literature search found more than 800 papers that prove at least one result only under the hypothesis or a stronger assumption that implies it.

OpenAI announced its result on October 26 in a paper titled “The Exponential Time Hypothesis is False.” It describes a deterministic algorithm that counts the satisfying assignments of such formulas in subexponential time while using a polynomial amount of memory. OpenAI said its model found the disproof on October 16 and that the company formalized it in Lean the next day.

Anthropic followed within a day, posting a paper credited to Claude, “A 2^o(n) Time Algorithm for 3-SAT,” along with its own Lean formalization. The paper says an internal Claude research model found the core algorithm on October 16 “with 14M output tokens and no human input,” and that Anthropic researchers then worked with the model on the presentation. It notes that, “independently and concurrently,” an OpenAI model claims to have proven a similar result.

Neither company claims a practical advance. Anthropic’s paper says that for 3-SAT formulas with five clauses per variable, its bound does not beat exhaustive search unless a formula has more than 10 to the power of 10,000 variables, and that “our result says nothing about solving formulas in practice.” OpenAI’s paper says the result does not imply that NP problems in general can be solved in subexponential time.

OpenAI said Impagliazzo, Paturi and MIT’s Ryan Williams will lead a group to verify and explain the result. In an open letter to the theoretical computer science community, the three wrote that “Our involvement should not be taken as certification of the claim” and asked researchers to help examine the proof. They also raised questions about early access to AI-generated results and credit. OpenAI agreed to the group’s request to fund a conference on the work.

A Lean check confirms that a formal statement has been proved but cannot show that the statement matches the paper. Anthropic’s repository says “no machine checks that this file says what the paper says” and keeps the file short so readers can check it against the paper.

OpenAI announced two other results the same day. It said its models proved the local smoothing conjecture in harmonic analysis in every dimension, which would also resolve the Kakeya and Stein restriction conjectures in all dimensions, and released the proof with a Lean version. It also claimed a rigorous existence proof for quantum chromodynamics and a unified completion of the Standard Model, including the existence of pure Yang-Mills theory, which is part of one of the Clay Mathematics Institute’s Millennium Prize problems. A group led by Nobel laureate David Gross will oversee that work and has chosen to withhold the AI-produced materials while it writes up the result.

OpenAI made a similar release in September, when it proposed a solution to the Navier-Stokes Millennium Prize problem and published a Lean formalization.

Sources: OpenAI, Anthropic, Reviewers’ open letter

–
By the Control Plane Editorial Team