ETH is false: two AI labs, two Lean proofs, one shared date

On October 26, OpenAI put a preprint titled The Exponential Time Hypothesis is False into its public math repository, with a Lean formalization beside it. Hours later, Anthropic published its own: A 2^o(n) Time Algorithm for 3-SAT, author "Claude (Anthropic)", in anthropics/formal-math. The Exponential Time Hypothesis — the 1999 assumption that 3-SAT needs exponential time in the number of variables, and the load-bearing wall under a large chunk of theoretical computer science — is, if both papers check out, false. I read both repositories on the 27th. Here is what is actually in them.

The two claims are not the same paper. OpenAI's preprint states a deterministic algorithm that, for every fixed k, exactly counts the satisfying assignments of k-CNF formulas in subexponential time and polynomial space. Anthropic's gives the sharper bound explicitly: #3-SAT in 2^O(n log log n / √log n), by way of tensor networks, rank decompositions, and — in its deepest appendix — the eight-square identity from 1818. Berkeley's Jelani Nelson, who read Claude's proof before release, says both proofs land at roughly exp(n/√log n) (CellCog's account). The discovery dates collide harder than the math: Anthropic's provenance line says its core algorithm was found on October 16 "with 14M output tokens and no human input," and notes the OpenAI model's result as "independent and concurrent." OpenAI's own post gives October 16 for its discovery too. Two labs, same day, each claiming independence — while Anthropic's Levent Alpöge had publicly suggested OpenAI was basing its solution on pre-existing work. Nothing in the public record settles it.

What "verified" means here, precisely: both proofs compile in Lean 4 against Mathlib. Anthropic's build takes about 8 minutes on 24 CPUs, depends only on Lean's three standard axioms, and gets re-checked against a second, independently written kernel. What no machine checks: whether the Lean statement is what the conjecture says. Anthropic's answer is a deliberately short statement file a human can read line by line. That caveat matters more coming from OpenAI, whose repository publicly withdrew three manuscripts on October 7 over a sign error and revised fourteen more — industrial-scale proof production has already failed once, visibly, three weeks ago.

What falls if the proofs stand: the Strong Exponential Time Hypothesis falls with ETH, since SETH implies it. Anthropic's paper counts more than 800 papers whose results rest on ETH or a hypothesis that implies it; all of them need new foundations or new proofs. Independent Set, Clique, Vertex Cover get subexponential algorithms on paper, and by Ryan Williams's 2013 theorem, E^NP gains a circuit lower bound. Williams — who put ETH's odds at 70% in 2019 — is now leading the working group examining the proof, alongside Russell Impagliazzo and Ramamohan Paturi, the hypothesis's own authors. Some parts of OpenAI's proof, he told TechCrunch, are routine; then there are "two or three alien-looking parts" the whole community needs to work on together.

What does not change: everything practical. The Anthropic paper is blunt — its bound does not beat brute-force search until n exceeds 10⁽¹⁰8) variables. Aggregators have been reporting "10^108"; the paper says 10 to the hundred-millionth. Brute force dies at n = 100; nobody is shipping a solver whose crossover is past the number of particles in the sky. P vs NP is untouched. And before anyone called their bank: Williams asked OpenAI's Dan Roberts whether any cryptosystem broke; they checked, and are "reasonably confident" nothing did.

The honest summary: a genuinely new kind of artifact — machine-found, machine-checked refutations of a standard assumption, released by rival labs hours apart, shepherded by the people who posed the problem. The refutation is verified inside Lean and unread by the community that lives on top of those 800 papers. Watch for the working group's readout, and for the first independent re-derivation. That, not the press release, is when ETH officially dies.