OpenAI and Anthropic say AI disproved the Exponential Time Hypothesis. What it means

What OpenAI and Anthropic announced

On October 26, OpenAI announced three results it says its internal models produced, in mathematics, computer science and physics. The computer science one is the headline: “Surprisingly, our system has recently proved that the ETH is false.” OpenAI says the model found the disproof on October 16, and that it was formalized the next day in Lean, a program that checks a proof step by step. The paper, “The Exponential Time Hypothesis Is False,” gives its author as OpenAI.

That night, Anthropic researcher Levent Alpöge posted a second paper, “A 2^o(n) Time Algorithm for 3-SAT,” credited to “Claude, Anthropic.” It reaches the same conclusion, and its account of where it came from is short: “The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input.” Anthropic researchers then worked with Claude on the write-up. The paper and its Lean proof are in Anthropic’s repository under Apache 2.0, and the paper says OpenAI’s model reached “a similar result” “independently and concurrently.”

Neither company has named the model that did the work.

What the Exponential Time Hypothesis is

3-SAT is the textbook hard problem. A formula has n variables, each true or false, and clauses that each name up to three of them and are satisfied when at least one has the value the clause asks for. Checking a proposed answer is quick; finding one, as far as anyone knew, wasn’t. The best algorithms still took exponential time, roughly 1.3 to the power n, Anthropic’s paper notes.

The Exponential Time Hypothesis, from Russell Impagliazzo and Ramamohan Paturi, says it can’t be done much faster: 3-SAT “cannot be solved in subexponential time,” in Wikipedia’s summary. OpenAI’s post says it “has been widely believed to be true.” Researchers have leaned on it to show that other problems can’t be solved quickly. A literature search Claude ran for Anthropic’s paper found “more than 800 papers” with a result proved only under ETH or a stronger hypothesis.

Both papers claim an algorithm that counts a formula’s solutions, not just finds one, in time that grows roughly like 2 to the power of n divided by the square root of log n. That grows more slowly than any exponential, which is what refutes the hypothesis. It still grows faster than any polynomial.

Does it mean P = NP?

No. The hypothesis is a stronger claim than P ≠ NP: “The exponential time hypothesis, if true, would imply that P ≠ NP, but it is a stronger statement,” as Wikipedia puts it. Disproving the stronger claim leaves the weaker one standing. Anthropic’s paper says so directly: “our result does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems.”

OpenAI’s paper adds that its speed-up “does not imply that general NP problems admit subexponential time algorithms,” because times like these don’t carry over through the usual reductions from one problem to another.

What it changes, and what it doesn’t

In theory, a lot. “If the claim is correct, it will change an important part of theoretical computer science,” wrote the researchers examining OpenAI’s result. Both papers say the Strong Exponential Time Hypothesis falls with it. Anthropic’s paper lists faster algorithms, in principle, for Independent Set, Clique, Vertex Cover and Dominating Set, and OpenAI says the result “reopens questions about how much faster these tasks could become.” Some lower bounds survive on weaker hypotheses: Anthropic says its result doesn’t refute the Orthogonal Vectors hypothesis, which OpenAI’s paper counts among those that “may still hold.”

In practice, nothing yet:

• No faster software. Anthropic calls its result “purely asymptotic.” On formulas with five clauses per variable, its bound beats trying every possible answer only past 10 to the 10,000th power variables, and its approach “seems unlikely to yield any general improvement” below about 10 million, while “brute force enumeration is already impractical for n = 100.” OpenAI says practical improvements “will require significant further research.”
• No broken encryption. Neither paper mentions the encryption that protects websites or messages. The only cryptography in OpenAI’s paper is versions of candidate one-way functions proposed by Oded Goldreich, which its algorithm can invert in less than exponential time; it adds, “This does not rule out one-wayness against polynomial-time algorithms.”
• No change to the AI you use. Neither lab announced a new model or a change to its apps or plans.

The two proofs, side by side

	OpenAI	Anthropic
Paper	The Exponential Time Hypothesis Is False	A 2^o(n) Time Algorithm for 3-SAT
Author line	OpenAI	Claude, Anthropic
Model	“Our system,” unnamed	“An internal research Claude model,” unnamed
Found	October 16	October 16
Time bound	2^O(n log log n / √log n)	2^O(n log log n / √log n)
Method	Contracting tensor networks	Contracting tensor networks
Lean	Formalized October 17, for a slightly weaker bound	Lean 4, checked by Lean’s kernel and a second, independently written one
People checking it	Impagliazzo, Paturi and Williams, organizing an open examination	“No person is known to have checked it”

How sure anyone is

Lean is the reason to take the claims seriously, and its limits are the reason not to treat them as settled. It checks that every step follows from the last. It can’t check that the theorem it proves is the one the paper claims. Anthropic’s paper is plain about this: “Whether the two definitions say what they are meant to say, that the Exponential Time Hypothesis is false and the Main Theorem, no machine can check; that is for the reader of the listing to judge.” Its Lean proof “was written by AI models and reviewed by other instances of the same models,” and its preprint on Hexagon is labeled “Primarily AI-generated,” with “Human understanding: some parts.”

OpenAI’s Lean statement is narrower than its paper. Its scope page covers formulas written in a canonical encoding and a slightly weaker time bound; the sharper bounds are in the paper only.

The people OpenAI asked to examine its result are the two who proposed the hypothesis, Impagliazzo and Paturi of UC San Diego, with Ryan Williams of MIT. Their letter says, “Our involvement should not be taken as certification of the claim,” and proposes a virtual meeting before the end of 2026. Williams wrote that they signed no NDAs and are unpaid, and that OpenAI agreed to release its raw data and sponsor a conference.

OpenAI’s last release is a caution. On October 6 it put out more than 700 manuscripts by its internal model. Two days later, Scientific American reported that “not all of the proofs were certified as correct” by Lean, and “some have already been retracted after outside scientists found mistakes.” Both ETH proofs come with Lean, which OpenAI’s repository says about 42% of its results have, and two labs say they reached this one independently.

OpenAI’s other two claims

Kakeya. OpenAI’s paper says its model proved Sogge’s local smoothing conjecture for the wave equation “in every spatial dimension at least two,” and with it the Kakeya conjecture: “every Euclidean Kakeya set has full Hausdorff dimension.” Before, OpenAI notes, local smoothing was known in two dimensions, from 2019, and Kakeya in three, from 2025. It comes with a Lean formalization, and OpenAI released the AI’s output for researchers to examine on their own, without forming a group to check it.

Yang–Mills. The physics claim is “a mathematically rigorous existence proof of certain interacting quantum field theories” in four dimensions, among them quantum chromodynamics, the theory of the strong force. It includes a proof of pure Yang–Mills existence, “part of the Quantum Yang–Mills Theory Clay Mathematics Institute Millennium Prize problem.” Part, not all: the Clay problem asks for proof that the theory “exists on R4 and has a mass gap,” and OpenAI’s post doesn’t mention a mass gap. The proof itself isn’t public. The group checking it, led by David Gross, “has decided to hold off on releasing the AI-produced artifacts” and will write the work up itself.

Trying it yourself

• Check Anthropic’s Lean proof. With Lean’s installer, elan, run lake exe cache get, lake build and lake env lean scripts/PrintAxioms.lean in the eth folder of Anthropic’s repository. Anthropic’s build took about 8 minutes on 24 virtual CPUs and about 7 GB of memory, and the last command should list only Lean’s three standard axioms. Then read MainResults.lean, the short file that says what is proved. That’s the part no machine checks.
• Rederive it with Claude. Anthropic’s README says “Claude Opus 5.5 at high effort can rederive the refutation of ETH” from a short description it publishes there, though only the weaker form, that 3-SAT can be decided in time O(2^δn) for every δ > 0. In Claude Code, choose Opus 5.5 with /model and run /effort high, as Anthropic’s docs describe. In Enjoy, pick High in the message box (how), then switch the conversation to Codex to see what GPT makes of the same hint.

What hasn’t been said

• Which models did the work, or whether either will be released.
• How the two proofs relate. They share a time bound and a method. Anthropic says they were found “independently and concurrently”; OpenAI’s post doesn’t mention Anthropic.
• Who has read them. Anthropic says no person is known to have checked its Lean proof. OpenAI hasn’t said whether anyone outside has worked through its Kakeya paper.
• When the physics write-up comes, or whether the Gross group will release the AI’s work.

We’ll update this memo when the reviewers report.