OrbitalHub

On October 26, 2026, OpenAI posted a preprint with a blunt title: The Exponential Time Hypothesis is False. The paper carried a date of October 17, a revision of October 25, a byline reading "OpenAI," and a Lean formalization in the company's public mathematics repository. Within hours, Anthropic published its own answer to the same problem, A 2^(o(n)) Time Algorithm for 3-SAT, with a Lean 4 development and build instructions. Both labs say a model found the result on October 16. The conjecture under attack was proposed in 1999, and much of complexity theory has leaned on it since.

The problem underneath is 3-SAT. An instance is a list of clauses, each one a disjunction of at most three literals over Boolean variables, and the question is whether some assignment of truth values satisfies every clause at once. Checking an assignment is trivial. Finding one by brute force means trying 2^n possibilities, and since 3-SAT is NP-complete, a polynomial-time algorithm for it would settle P versus NP the other way. The Exponential Time Hypothesis is a sharper bet. Put s₃ for the infimum of all exponents δ such that some algorithm decides 3-SAT on n variables in time O(2^(δn)). ETH says s₃ > 0: some fixed positive δ sits out of reach, so 3-SAT always costs a constant fraction of the full exponential. Russell Impagliazzo and Ramamohan Paturi proposed the hypothesis in 1999 and refined it with Francis Zane in 2001.

What makes it more than a guess about one problem is how much rests on it. ETH implies P ≠ NP, and its negation does not imply P = NP. Under ETH, k-Clique has no algorithm running in f(k) n^(o(k)) time, dynamic programming on bounded treewidth is optimal up to a log factor, and a long list of parameterized algorithms is optimal in the exponent. ETH also underwrites conditional circuit lower bounds: a theorem of Ryan Williams says that if ETH is false, the class E^NP has no linear-size Boolean circuits. Impagliazzo called the hypothesis a "principled educated guess" and put the odds at "a fair coin flip" in a 2012 lecture; Williams gave ETH about 70 percent odds of being true in 2019.

Both labs announced within hours of each other, and both shipped Lean proofs. OpenAI's route was to enlist the people who know the terrain. Impagliazzo and Paturi at UC San Diego, who proposed the hypothesis, and Williams at MIT, who had already refuted strong versions of it, now lead an open examination of the claim, with a conference funded by OpenAI to work through the fallout. Williams told TechCrunch that in the OpenAI proof some parts are routine, "but then yes, there are two or three alien-looking parts," and those are the pieces that convinced him the field needs to look at them together. His first question to OpenAI's science lead Dan Roberts was whether any cryptographic system is now insecure; they had checked, he reports, and were reasonably confident nothing breaks. The release ran wider than 3-SAT: OpenAI also claimed the local smoothing conjecture in every dimension, which implies Kakeya, and existence for Yang-Mills theory in four dimensions, settling half of a Clay Millennium Prize problem. That manuscript stays with the group David Gross leads, a choice OpenAI's advisory panel has publicly opposed.

Anthropic's artifact is unusually well documented. Its paper, posted on the Hexagon preprint server under a CC BY licence, states the result in the abstract: a deterministic algorithm for 3-SAT running in 2^(o(n)) time, which also counts satisfying assignments, the harder #3-SAT problem. The provenance statement says the core algorithm was found on October 16 by an internal Claude research model using 14 million output tokens and no human input, after which Anthropic researchers worked with Claude on the write-up. The GitHub repository pins Lean 4.33.1 and the matching Mathlib, explains how to build the development, and notes that a second, independently written kernel called nanoda re-checks the proofs alongside Lean's own. The README reports 1,050 modules, written by AI models and reviewed by other instances of the same models. Its strangest entry is a condensed description of the proof, enough, the README says, for a current Claude model to rederive the refutation on demand.

The mathematics behind Anthropic's paper starts with the sparsification lemma, which lets you assume the formula is sparse, so its clause count is proportional to its variable count. The counting problem then becomes a sum of products over a graph whose nodes are clauses and whose edges carry the shared variables, and it can be split recursively as long as the bits crossing each cut stay few. The lever that makes it work is an identity two centuries old: Degen found it in 1818, Graves rediscovered it in 1843 through the octonions, and it says a match between two pairs of 3-bit vectors can be written as a product of sign functions, 2[x=v][y=u] = [x⊕y⊕u⊕v=0](σ(x,y)σ(v,u) + σ(x,u)σ(v,y)), where σ is a table of plus and minus signs. It spans 12 bits and can be checked at all 4,096 settings. Laying the two terms out as a grid turns each crossing into a choice between merging rows and merging columns, and iterating that, with pieces built at rate ρ = 1/√2, yields a runtime of 2^{O(min{km/√(log m), k²n log log n/√(log n)})}.

OpenAI's paper reaches the same conclusion by a different road, giving a deterministic algorithm that counts satisfying assignments exactly, built from polynomial interpolation and sparse parity tests on low-degree forms, running in (n+m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}} time with polynomial space. Both results are asymptotic in a way that matters: Anthropic's bound, for a formula with the usual five clauses per variable, does not beat exhaustive search until the variable count passes 10^(10,000), and its bound in n alone does not bite until n passes 10^(100 million). Brute force is already unusable at 100 variables. Neither paper makes anything faster in practice.

What the Lean files do and do not establish is worth sitting with. Anthropic's MainResults.lean holds no proofs at all, only definitions: def ETH : Prop := 0 < s 3 and def ETHIsFalse : Prop := ¬ ETH, followed by the main counting theorem. The proofs live in a separate file, and the README is blunt about the limit of machine checking: "Lean checks the proofs, but no machine checks that this file says what the paper says." The formalization proves the stated proposition, not that the stated proposition is what the field means by ETH, and that gap is now a human responsibility. The paper's appendix adds that the Lean development was written by AI models, reviewed by other models, and that no person is known to have checked it. OpenAI's side has the same shape and a bigger pile: 721 manuscripts in 373 families, some formalized and some not, produced by posing roughly 4,000 problems to an unreleased model, each result averaging about three hours of thinking compute.

The consequences, if the work holds, are wide and uneven. The counting corollary gives s_k = 0 for every k ≥ 3, so s_∞ = 0 and both ETH and SETH are false. A literature scan carried out by Claude turned up more than 800 papers that prove a result of their own only under ETH, or under a hypothesis implying it. The Orthogonal Vectors hypothesis is untouched, though, and many fine-grained lower bounds rest on that rather than on ETH, so a large share of the lower-bound literature survives. P versus NP survives with it, with Williams describing the effect as a shift in priors rather than a solution.

What changed most is procedural. Two frontier labs have put the same kind of artifact in public view on the same day: a theorem the field spent decades formulating, a proof written by a model, and a machine-checked formalization that settles the steps but not the meaning. The checking is being organized as a community practice, with the proposers of the hypothesis running the examination. Credit is not, and the release policy is still being argued over in public, which is why the advisory panel OpenAI convened has been pressing for the physics manuscript to be released.