Same Day, Same Conjecture: OpenAI and Anthropic Both Say Their AI Refuted the Exponential Time Hypothesis

For a quarter of a century, theoretical computer science has leaned on an assumption almost nobody expected to fall: that 3-SAT cannot be solved in time 2^o(n). This week two AI labs say their models knocked it down, independently, and both say the key step was found on the same day.

On Monday, 26 October 2026, OpenAI published a batch of results produced by what it calls “an unnamed internal OpenAI model”, headlined by three claims: a refutation of the Exponential Time Hypothesis (ETH), a proof of the local smoothing conjecture in harmonic analysis (which would imply the Kakeya and Stein restriction conjectures), and an existence proof for four-dimensional Yang–Mills theory and QCD. Within hours, Anthropic posted a paper of its own on the Hexagon preprint server, titled “A 2^o(n) Time Algorithm for 3-SAT” (version 1 dated 27 October). Its provenance note reads: “The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input.” OpenAI’s account also dates its ETH disproof to 16 October, with a Lean formalisation the next day.

This post concentrates on the ETH claim, because it is the one that touches computer science most directly and the one where both labs have released checkable artifacts.

What ETH says, and why it mattered

ETH was formulated by Russell Impagliazzo and Ramamohan Paturi (with Francis Zane on the companion paper) around 2000. Informally: there is a constant δ > 0 such that 3-SAT on n variables cannot be solved in time 2^δn. In other words, satisfiability is not just hard; it is exponentially hard, and no clever algorithm can shave the exponent down to something sublinear in n. The best practical worst-case algorithms for 3-SAT run in about 1.3ⁿ, which is exponential and consistent with ETH.

ETH is stronger than P ≠ NP, and that is what made it useful. Hundreds of results in parameterized and fine-grained complexity are conditional lower bounds of the form “assuming ETH, problem X has no 2^o(k) algorithm”. When researchers wanted to argue that their exponential algorithm for some graph problem was essentially optimal, ETH was the standard foundation. If ETH is false, those statements are not wrong, but they become implications from a false premise and say nothing.

What the two labs actually claim

OpenAI. The Lean scope document in OpenAI’s public openai/math GitHub repository states: for every fixed k ≥ 2, a deterministic machine exactly counts the satisfying assignments of a k-CNF formula on n variables in time (L+1)^O_k(1) · 2^{O_k(n (log log n)² / √log n)}, where L is the input’s bit length, while visiting only polynomially many tape cells. The 25 October manuscript claims a sharper exponent, n·log log n / √log n, and 2^{O(n/√log n)} for formulas with a bounded clause-to-variable ratio. Commentators tracking the claim note that only the weaker bound is covered by the Lean theorem; the sharper ones rest on the written proof.

Anthropic. The abstract is short: “We refute the Exponential Time Hypothesis (ETH) by presenting a deterministic algorithm for 3-SAT on n variables that runs in 2^o(n) time. Our algorithm in fact solves the harder problem #3-SAT… and has been formalized in Lean 4.” The page carries the labels “Primarily AI-generated text” and “Human understanding: some parts”. It also notes that OpenAI claims a similar result.

Two details matter for a developer reading this. First, both algorithms count solutions rather than merely deciding whether one exists. Counting is at least as hard as deciding, so this is the stronger claim. Second, both are deterministic, with no randomisation to argue about.

What Lean certifies, and what it doesn’t

A Lean proof that compiles means the formal statement follows from the axioms and the library. It does not mean the formal statement is the theorem you think it is. A machine model can be defined slightly wrong, an encoding can quietly smuggle in an assumption, and the headline bound in the PDF can be stronger than the one the kernel actually checked. That last gap already exists on the OpenAI side. This is why the formalisation is necessary but not sufficient, and why human experts still have to read the statement line by line.

There is also an incentive problem. OpenAI’s repository describes its whole drop (721 manuscripts across 373 families, from roughly 4,000 problems at an average of three hours of ChatGPT Pro thinking compute each) as “raw research data, rather than polished academic papers”, and warns that “some of the unformalized results could have issues”. That honesty is welcome. It also means the review burden has moved onto the research community.

Why this changes nothing for your SAT solver, and possibly a lot for theory

A 2^{n/√log n} bound is subexponential, but it is still super-polynomial, and the constants hidden in the O_k(·) are unknown and probably enormous. Reporting on the claim agrees that it offers no practical speedup at any size a computer could handle. Your CDCL solver, your package-manager dependency resolver and your SMT-based verifier are unaffected. Cryptography is not broken. Deployed schemes do not rely on ETH, and no source suggests otherwise. Refuting ETH also does not settle P vs NP.

The real impact is on theory. If the result holds, every ETH-conditional lower bound needs a new foundation. The obvious candidates are weaker assumptions, or hypotheses about other problems, and the field will have to work out which ones survive. It would also be the first time a machine, rather than a human with machine help, overturned a foundational complexity conjecture. And two labs reaching it independently the same week makes a lucky fluke less plausible.

The scepticism is deliberate

The three people best placed to judge the result, Impagliazzo and Paturi (UC San Diego) and Ryan Williams (MIT), are shepherding the review. They wrote: “Our involvement should not be taken as certification of the claim. A result of this significance requires careful, independent scrutiny.” OpenAI agreed to release the raw data and to fund a conference on the result, and separately gave $5 million to the Simons Foundation for workshops on AI-produced mathematics.

The other two claims are on weaker footing. The local smoothing proof is public, and harmonic analyst Alex Iosevich called it a “historic development”. But the claimed scope of its Kakeya and Stein consequences varies between OpenAI’s own sentences. The Yang–Mills/QCD result is the least documented. A group led by David Gross is writing it up and the AI materials have not been released, which prompted Timothy Gowers and the Advisory Group on Mathematics and AI to publicly ask for them. It is also an existence result. Nothing published so far claims the mass gap, which is the actual Clay Millennium Prize problem.

As of today, no independent verdict has been published on any of the three results. The right reading is “very serious claim with checkable artifacts”, not “theorem”.

What to watch

The Impagliazzo–Paturi–Williams group’s verdict, and whether the sharper manuscript bound gets formalised.
Whether the two algorithms share a core idea. If they do, a single flaw sinks both. If they differ, that is strong corroboration.
Release of the Yang–Mills materials, and how journals and arXiv handle “primarily AI-generated” mathematics.
How quickly OpenAI and Anthropic turn this kind of research model into products. The “14M output tokens, no human input” line is the part an engineering manager should remember.