OpenAI and Anthropic Refute ETH on the Same Day: Complexity Formulas, Lean Proofs, and Verification Status

Posts circulated online claiming that an OpenAI model had refuted the Exponential Time Hypothesis (ETH), one of the central conjectures in computational complexity theory.
ChatGPT confirmed that OpenAI made the announcement on October 26, 2026.
However, while ChatGPT cited specific complexity formulas, it was difficult to tell how accurately those claims mirrored the original papers.
To verify the formulas and background, I examined OpenAI’s announcement, the paper preprints, the Lean formal proofs, and statements from external researchers coordinating the review.
It turned out that Anthropic had published an independent refutation achieving the same asymptotic complexity just hours after OpenAI.

ETH is a Conjecture About 3-SAT

The Exponential Time Hypothesis (ETH) addresses the algorithmic difficulty of solving 3-SAT.
In 3-SAT, an algorithm receives $n$ Boolean variables $x_1, \ldots, x_n$ and a formula formed by taking the conjunction (AND) of clauses, where each clause contains at most three literals joined by disjunction (OR).
A literal is either a variable $x_i$ or its negation $\lnot x_i$, yielding formulas such as $(x_1 \lor \lnot x_2 \lor x_3) \land (\lnot x_1 \lor x_4)$. The problem asks whether there exists a truth assignment that satisfies every clause simultaneously, and it is a canonical NP-complete problem.

The simplest approach is brute-force search across all variable assignments.
Because each variable can be either true or false, there are $2^n$ possible assignments to test.
Evaluating a single assignment takes time proportional to the length of the formula, resulting in an overall running time of approximately $2^n \cdot \mathrm{poly}(n, m)$, where $\mathrm{poly}(n, m)$ is a polynomial factor in $n$ and clause count $m$.

Algorithms faster than brute-force search have long been known.
Representative algorithms cited in the related work section of OpenAI’s paper exhibit the following running times when converted to base-2 exponents:

Algorithm	Type	Running Time	Base-2 Form
Brute force	Deterministic	$2^n$	$2^{1.000n}$
Schöning local search (1999)	Randomized	$(4/3)^n$	$2^{0.415n}$
Liu (2018)	Deterministic	$1.32793^n$	$2^{0.409n}$
Improved PPSZ (Jiang & Cai preprint)	Randomized	$1.307031578^n$	$2^{0.386n}$

While each algorithm improves upon $2^n$, the running time still scales by a fixed multiplicative constant every time $n$ increases by 1.
ETH asserts that no algorithm can escape this exponential baseline.
Under the formal definition introduced by Impagliazzo and Paturi in 2001, $s_3$ is defined as the infimum of constants $\delta$ for which 3-SAT can be solved in $O(2^{\delta n})$ deterministic time. ETH states that $s_3 > 0$.
In other words, there exists some positive constant $\delta$ below which no algorithm can run.

Refuting ETH requires demonstrating that for every $\delta > 0$, no matter how small, there exists an algorithm that solves 3-SAT in $O(2^{\delta n})$ time.
A single algorithm running in $2^{o(n)}$ time suffices to refute the hypothesis.
Here, $o(n)$ denotes a function that tends to 0 when divided by $n$ as $n \to \infty$. Because the exponent divided by $n$ vanishes asymptotically, the running time eventually drops below $2^{\delta n}$ for any fixed $\delta > 0$.

Complexity Bounds Claimed in the Papers

OpenAI’s preprint, titled “The Exponential Time Hypothesis is False”, introduces an algorithm that decides 3-SAT and counts the total number of satisfying assignments (#$k$-SAT). Determining whether the count exceeds zero immediately yields a decision algorithm.
The algorithm targets formulas in $k$-CNF where each clause has at most $k$ literals, holding $k \ge 2$ fixed as $n \to \infty$. The preprint is dated October 17, 2026, with revisions dated October 25.

The abstract states the running time with polynomial memory in $n$ and $m$ (where $O_k(1)$ is a constant depending on $k$):

$$(n+m)^{O_k(1)} \, 2^{\,n/(\log n)^{1/2+o(1)}}$$

Theorem 1.1 formalizes this into two concrete upper bounds (with $\log$ denoting the natural logarithm):

Conditions	Running Time Upper Bound
General $k$-CNF	$(n+m)^{O_k(1)} \, 2^{O_k(n \log\log n / \sqrt{\log n})}$
Clause count bounded by $m \le Dn$ ($D$ constant)	$(n+m)^{O_{k,D}(1)} \, 2^{O_{k,D}(n / \sqrt{\log n})}$

When the clause count is linear in the number of variables, the running time simplifies to $2^{O(n/\sqrt{\log n})}$. In the general case, an extra factor of $\log\log n$ appears.

Because the algorithm counts solutions, it also refutes #ETH, the counting analogue of ETH that conjectures #3-SAT requires $2^{\Omega(n)}$ time.
The result applies to $k = 2$ as well. While deciding 2-SAT runs in linear time, counting satisfying assignments (#2-SAT) is #P-complete and requires exponential time under standard assumptions. OpenAI’s paper directly compares its bound against Wahlström’s $O^*(1.2377^n)$ counting algorithm.

Verifying Whether the Exponent is in o(n)

Dividing the exponents by $n$ produces $1/\sqrt{\log n}$ and $\log\log n/\sqrt{\log n}$.
Because $\log n$ grows significantly faster than $\log\log n$, both ratios approach 0 as $n \to \infty$.
I computed the limits in SymPy, including the weaker $(\log\log n)^2$ bound from the Lean formalization:

import sympy as sp
n = sp.symbols('n', positive=True)
L = sp.log(n)
for e in [n/sp.sqrt(L), n*sp.log(L)/sp.sqrt(L), n*sp.log(L)**2/sp.sqrt(L)]:
    print(e, sp.limit(e/n, n, sp.oo))

All three limits evaluate to 0.
Each bound belongs to $2^{o(n)}$. Multiplying by the polynomial factor $(n+m)^{O(1)}$ does not change the asymptotic outcome because the number of distinct clauses in 3-SAT is bounded by a polynomial in $n$. If the mathematical arguments hold, ETH is formally false.

Why Sub-Exponential Does Not Mean Practically Fast

A running time in $2^{o(n)}$ implies that the exponent grows slower than $n$, but it does not mean the actual operation count is small for manageable input sizes.
Assuming the implicit constant in $O(\cdot)$ equals 1, computing the exponent divided by $n$ with Python’s arbitrary-precision library mpmath yields:

$n$	$1/\sqrt{\log n}$	$\log\log n/\sqrt{\log n}$	$(\log\log n)^2/\sqrt{\log n}$
$10^{3}$	0.381	0.735	1.421
$10^{6}$	0.269	0.706	1.855
$10^{9}$	0.220	0.666	2.018
$10^{100}$	0.066	0.358	1.950
$10^{1000}$	0.021	0.161	1.249
$10^{10000}$	0.0066	0.066	0.665

Even at $n = 10^9$, the fastest-decaying factor $1/\sqrt{\log n}$ only reaches 0.22.
This is close to the 0.386 exponent of existing PPSZ variants, and constants can easily flip the advantage. For the Lean formalization bound in the rightmost column, the ratio only dips below 1 when $\log n \approx 5504$, corresponding to $n \approx 10^{2390}$.

Anthropic’s paper calculates the constants for its own bound.
Even on 3-CNF formulas with $m = 5n$, their algorithm requires $n > 10^{10000}$ variables before beating $2^n$ brute force, and requires $n > 10^{10^8}$ when clauses are unrestricted. Because brute force is already intractable at $n = 100$, the authors state that the algorithm does not function as a practical tool at this scale. OpenAI’s announcement also noted that translating theoretical progress into practical algorithms will require further research.

Timeline Leading to the Announcements

Tracking OpenAI’s post, “Working with academic communities to build scientific understanding”, the commit history of openai/math, and Anthropic’s paper yields the following timeline:

Date (US Time)	Event	Source
September 9	OpenAI model outputs natural language existence proof for pure Yang-Mills	OpenAI post
September 18	Model outputs existence proof for QCD	OpenAI post
October 6	OpenAI releases batch of internal math papers (721 papers across 373 topics)	openai/math README
October 7	OpenAI retracts 3 papers due to sign errors	history.md
October 16	OpenAI model outputs natural language ETH refutation	OpenAI post
October 16	Anthropic’s internal Claude model identifies core refutation algorithm	Anthropic paper
October 16	OpenAI completes Lean formalization of Yang-Mills existence proof	OpenAI post
October 17	OpenAI completes Lean formalization of ETH refutation	OpenAI post
October 18–19	Model outputs proof of local smoothing conjecture; formalized in Lean next day	OpenAI post
October 26	OpenAI announces 3 results, posting ETH paper and Lean code on GitHub	OpenAI post, repo
October 26 night	Anthropic publishes paper and Lean proof on anthropics/formal-math	Repository commit

OpenAI pushed its repo updates at 21:18 UTC on October 26, while Anthropic committed its repository at 03:07 UTC on October 27, an approximate six-hour gap between the releases.
According to Anthropic’s paper, Claude generated the algorithmic breakthrough across 14 million output tokens without human guidance, after which Anthropic researchers organized the paper structure around the model’s outputs. The preprint cites OpenAI’s concurrent discovery as an independent validation of similar techniques.
TechCrunch reported that Anthropic mathematician Levent Alpöge pointed out connections between OpenAI’s preprint and existing literature shortly before Anthropic published its own proof.

The bound stated in Anthropic’s README is $2^{O(n \log\log n/\sqrt{\log n})}$, matching OpenAI’s Theorem 1.1 for general $k$-CNF. Anthropic’s Theorem 1 takes the minimum between this and a clause-dependent bound $2^{O(km/\sqrt{\log m})}$.
The techniques also diverge: OpenAI emphasizes sparse parity checks and polynomial interpolation, whereas Anthropic centers its reduction on tensor network contraction.

How the Review is Organized

OpenAI organized its announcement across three distinct scientific areas, assigning external “shepherds” to lead community verification and adopting different publication strategies:

Field	Claimed Result	Release Strategy
Mathematics	Proof of the local smoothing conjecture in all dimensions (implying Kakeya and Stein restriction)	Raw model output released publicly for open verification
Computer Science	Refutation of ETH	External group coordinates review; AI output released immediately
Physics	Mathematical existence of 4D quantum field theories for QCD and unified models	External group writes independent review; raw AI output withheld

The ETH verification group is led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, alongside Ryan Williams of MIT. Impagliazzo and Paturi originally formulated ETH with Francis Zane in 2001. Williams previously disproved several stronger variants of ETH, including disproving the Merlin–Arthur variant of SETH in 2016.

The verification operates under four ground rules: participants sign no non-disclosure agreements (NDAs) and can discuss findings openly; OpenAI seeks no academic authorship or credit; participation is voluntary and unpaid; and any conclusions are the researchers’ independent views rather than OpenAI’s stance.

On X, Williams referred to the work as a “claimed refutation.” In follow-up posts, he highlighted that operating without NDAs enables immediate open discussion. He requested that OpenAI immediately publish raw materials, including PDFs and Lean source code, and asked OpenAI to fund an academic workshop for affected researchers, both of which OpenAI agreed to support.

The three organizers issued an open letter stating: “Our involvement should not be taken as certification of the claim.” The letter invites researchers to coordinate verification tasks and discuss access and attribution protocols for AI-generated discoveries. The letter’s bibliography includes links to both OpenAI’s preprint and Anthropic’s refutation.

Why Verification is Necessary Despite Lean Proofs

Lean is a formal proof assistant that verifies whether a mathematical derivation rigorously establishes a given theorem statement. However, the machine only verifies that the formal proof matches the stated proposition; determining whether that proposition accurately reflects the mathematical claim of the paper still requires human review.
Anthropic’s README emphasizes this distinction, explaining that MainResults.lean deliberately avoids external imports beyond Mathlib and lists divergences from the main text in Appendix E so readers can inspect the correspondence directly.

Both organizations used Comparator, a verification tool developed by leanprover, to establish standardized auditing conditions. The tool isolates the theorem statements in a “challenge” file from the proof implementation, verifies that the proof matches the challenge, and checks that it relies strictly on authorized foundational axioms. In both repositories, proofs are restricted to Lean’s three standard axioms: propext, Quot.sound, and Classical.choice. In Lean, introducing an arbitrary unverified axiom (such as asserting falsehood) trivializes proof checking, so this restriction is necessary.
Anthropic additionally verified its proof using nanoda, an independent Lean kernel implementation, while OpenAI’s configuration relied on the standard Lean kernel.

The theorem formulations also differ. Anthropic defines $s_3$ and asserts ETH : Prop := 0 < s 3, and then proves its negation ETHIsFalse under a Turing machine model from Mathlib. OpenAI’s challenge file, SubexponentialSAT.lean, does not name ETH directly, but rather proves that a machine correctly outputs the count of satisfying assignments for any $k$-CNF within specified sub-exponential time and polynomial space bounds. Disproving ETH follows as an immediate corollary.

Differences Between the Lean Bound and the Paper Bound

According to the formalization documentation in OpenAI’s repository, the bound formalized in Lean is:

$$(L+1)^{O_k(1)} \, 2^{O_k(n (\log\log n)^2 / \sqrt{\log n})}$$

where $L$ denotes the bit length of the input.
Compared to the general bound in the paper, the exponent contains $(\log\log n)^2$ instead of $\log\log n$. The preprint text explains that polynomial interpolation yields $n(\log\log n)^2/\sqrt{\log n}$, while the tighter bounds are derived via tensor contraction in the appendix.
As verified in the SymPy calculations, this weaker bound still approaches 0 when divided by $n$, which is sufficient to refute ETH. The sharper bound claimed in the paper remains outside the formalized code for now.

Implications if the Results Hold

Synthesizing the preprints and commentary outlines the anticipated mathematical impact:

Target	Status if Validated	Basis
ETH	Refuted	Both preprints
SETH (Strong ETH)	Refuted	SETH implies ETH; refuting ETH invalidates SETH
#ETH, Gap-ETH, NSETH	Refuted	OpenAI preprint (covering approximation and non-deterministic forms)
Orthogonal Vectors Hypothesis (OV)	Not refuted	Anthropic preprint (finding orthogonal vector pairs)
P vs NP	Unresolved	Both preprints
General NP-complete problems	Not necessarily $2^{o(n)}$	OpenAI preprint
Practical SAT solvers	Unaffected	Anthropic preprint, OpenAI post
Practical cryptography	No direct threat	TechCrunch reporting

SETH conjectures that $k$-SAT cannot be solved in $2^{(1-\varepsilon)n}$ time as $k \to \infty$. Because SETH implies ETH, disproving ETH automatically disproves SETH.
Conversely, the Orthogonal Vectors hypothesis, which underpins lower bounds in fine-grained complexity, is implied by SETH rather than implying it; the problem remains open. Anthropic’s preprint notes that over 800 papers establish conditional lower bounds reliant on ETH or its direct implications.

While NP-complete problems reduce to each other in polynomial time, OpenAI’s paper cautions that sub-exponential running times of $2^{o(n)}$ are not preserved under arbitrary polynomial reductions. If a reduction maps an instance with $n$ variables to one with $n^2$ variables, a running time of $2^{o(n^2)}$ is no longer sub-exponential in the original size $n$. Consequently, the refutation does not imply sub-exponential algorithms for all NP-complete problems. Sub-exponential bounds only transfer to problems reducible with nearly linear variable blowup, such as chromatic number or counting perfect matchings.

Regarding cryptography, Williams stated to TechCrunch that while algorithmic refinements might eventually affect specific key lengths, OpenAI’s Dan Roberts indicated that internal analysis found no threat to modern cryptosystems. RSA relies on the hardness of integer factorization, which is not known to be NP-complete and is already subject to sub-exponential methods like the general number field sieve (as explored in my previous article on factoring RSA-260). Williams added that computer scientists should place slightly higher probability on P = NP, while noting he does not believe the current algorithms are the theoretical optimum.

The Other Two Simultaneous Announcements

The mathematical result proves Sogge’s 1991 local smoothing conjecture in all dimensions. This formalizes the principle that wave concentrations disperse almost instantaneously. If verified, it establishes both the Kakeya conjecture and the Stein restriction conjecture. Special cases had been established previously: the 2D case by Guth, Wang, and Zhang in 2019, and the 3D Kakeya conjecture by Wang and Zahl in 2025. Both the paper and Lean code are available in OpenAI’s repository.

The physics result claims a rigorous mathematical construction of interacting quantum field theories in four dimensions involving gauge fields and fermions, covering QCD and unified field theories while establishing the existence of pure Yang-Mills theory as an intermediate lemma. Yang-Mills existence is an unsolved Millennium Prize problem. A research group led by David Gross is reviewing the derivation and writing an independent exposition, during which the raw model output remains private.

Comparing Initial Rumors with Original Sources

Initial summaries from ChatGPT aligned with the broad narrative: the timeline (October 16 discovery, October 17 Lean formalization, October 26 announcement), the trio of shepherds, the absence of NDAs or compensation, the divergence between the Lean bound and paper bound, and the fact that P vs NP remains open.
However, examining the original sources revealed several key nuances absent from early online claims:

Initial Rumors & Chat Summaries	Findings from Original Sources
Running time stated generally as $2^{O(n/\sqrt{\log n})}$	This bound requires clause sparsity $m \le Dn$. General formulas incur an extra $\log\log n$ factor
ETH defined as “cannot be solved fundamentally faster than exponential time”	Formally, ETH asserts that $s_3 = \inf\{\delta \mid O(2^{\delta n})\} > 0$. Existing algorithms at $1.307^n$ remain exponential
OpenAI fully funded the entire conference	OpenAI committed to sponsoring an academic workshop without specifying total amounts or full coverage
Practical speedups for SAT solvers left ambiguous	Anthropic calculated its bound only beats brute force when $n > 10^{10000}$, and stated that no practical speedup exists
Unmentioned in initial discussions	Anthropic independently discovered the algorithm on October 16 and published its refutation and Lean proof hours later
Unmentioned in initial discussions	Both organizations verified proofs using Comparator, and strictly limited axioms to standard Lean foundations