OpenAI and Anthropic say their AIs disproved a key hypothesis in computer science

On October 26, OpenAI posted a document with an unequivocal title: “The Exponential Time Hypothesis is False.” On October 27, Anthropic published its own article, signed “Claude (Anthropic),” making the same claim. Both companies say their internal, unreleased model found the central idea on October 16.

Each text comes with a proof formalized in Lean, software that mechanically checks every step of a mathematical argument. Neither has yet been validated by the scientific community.

A hypothesis on which hundreds of papers rest

Formulated in the late 1990s by Russell Impagliazzo and Ramamohan Paturi, together with Francis Zane, the Exponential Time Hypothesis (ETH) concerns a famous logic problem, 3-SAT: can variables be assigned the value “true” or “false” so as to satisfy a list of constraints, each involving three of them? The hypothesis states that no algorithm can do this without a running time that multiplies by a fixed factor with each added variable.

Researchers use it to prove that problems in graph theory, biology or databases cannot be solved quickly. According to Anthropic's article, more than 800 papers depend on it, directly or through a related hypothesis. Both labs describe an algorithm that solves 3-SAT, and even counts its solutions, in so-called “subexponential” time. Jelani Nelson, a Berkeley computer scientist on leave from the university to work at Anthropic, submitted the company's paper to the Hexagon platform and reviewed its proof before publication. According to him, the two proofs arrive at roughly the same bound.

Who is checking these proofs?

OpenAI entrusted its result to three specialists: Russell Impagliazzo and Ramamohan Paturi, the authors of the hypothesis, from the University of California, San Diego, and Ryan Williams of MIT. In an open letter, they warn that their involvement “should not be considered a certification.” According to The Next Web, Ryan Williams says they signed no nondisclosure agreement and will not be paid. OpenAI says it claims no academic credit and gave $5 million to the Simons Foundation for workshops on AI-produced results.

At Anthropic, the warning appears in the code repository itself: the Lean formalization “was written by AI models,” and no machine checks that its statement says what the paper says; that check falls to a human reader. An appendix to the paper specifies that the formalization has only been reviewed by other instances of the same models and that, at the time of writing, no person is known to have verified it.

OpenAI also claims two other results, in analysis and theoretical physics. The second touches one of the Clay Institute's “Millennium Problems,” but its documents are not public: the group of physicists led by Nobel laureate David Gross chose to write up its conclusions itself.

Nothing changes for software or encryption

“If the claim is correct, it will change an important part of theoretical computer science,” write OpenAI's three reviewers. In practice, though, nothing moves. Anthropic's repository says so bluntly: the result “says nothing about solving formulas in practice.” According to the paper, for a formula with five times as many constraints as variables, the algorithm beats exhaustive search only beyond 10^10,000 variables. The “P = NP?” question remains open. Encryption is not under threat: factoring, on which RSA relies, has been done in subexponential time for decades, and key sizes take that into account.

That leaves the coincidence: two rival models, the same discovery, the same day. Jelani Nelson pointed it out on X. This is not the two labs' first foray into this field: they are already funding the verification of AI-written proofs. OpenAI's reviewers worry that credit will go to whoever publishes first or has the most powerful tools, rather than to those who verify and explain; in June, mathematicians had already raised the question of attribution in the “Leiden Declaration.” The upcoming workshops will show whether the proof withstands human scrutiny.