OpenAI Claims Its Model Falsified the Exponential Time Hypothesis. The Verifying Starts Now.

OpenAI announced on October 26 that an internal, unreleased reasoning model has produced three results it is submitting to academic communities for verification, and the headline claim is as large as claims get: a preprint dated October 25 describes a 2^o(n)-time algorithm for 3-SAT, which, if correct, falsifies the Exponential Time Hypothesis, the assumption underlying hundreds of conditional lower bounds across fine-grained complexity theory. The paper sits in OpenAI’s public math repository alongside dozens of other model-produced preprints, including claimed counterexamples to Hadwiger’s conjecture and the Baum-Connes injectivity statement. OpenAI says the ETH algorithm is machine-verified in Lean. The announcement, made in a post titled “building scientific understanding with academic communities,” describes a shepherding process in which academic partners check results before wider acceptance. The thread attracting 597 points on Hacker News overnight is appropriately split between amazement and the only correct initial posture: this is a claim, not a settled result.

What is actually claimed, in the precise terms

The Exponential Time Hypothesis asserts that 3-SAT cannot be solved in 2^o(n) time in the number of variables; it is weaker than P versus NP but stronger in practical reach, since it underpins conditional lower bounds for dozens of problems via reductions. A 2^o(n)-time 3-SAT algorithm would not make SAT easy in any usable sense; the Hacker News consensus, including complexity researchers, is that the algorithm is described as totally impractical, with enormous constants. What it would do is invalidate a proof technique: hundreds of published results of the form “no algorithm for X runs in 2^o(n) unless ETH fails” would lose their foundation. The related claims in the announcement include a natural-language proof for Yang-Mills existence (dated September 9, one of the Clay Millennium problems) and a Kakeya-set-related result, plus an improved 3SUM algorithm at O(n^1.9992). The verification status differs by claim: the ETH algorithm is stated as Lean machine-checked, while the Yang-Mills proof is natural-language and would require human mathematical review.

The reason for calibrated skepticism is OpenAI’s own record

The shepherding process is the right mechanism, and its need is demonstrated by OpenAI’s own precedent: the same unreleased model previously produced a dump of 722 manuscripts grouped into 372 result families, of which three were withdrawn after a sign error invalidated one argument and two papers depending on it, and 14 were revised. Extraordinary titles in the public repository, including a claimed counterexample to Hadwiger’s conjecture, carry the same burden. Machine-checking in Lean is the strongest available form of verification for a formal argument, the same toolchain Anthropic used for assembly-level memory-safety proofs last week, but it verifies the theorem as stated, not whether the statement says what the announcement implies; subtle mismatches between a formalized claim and its intended meaning have a history. The shepherd process, where domain experts formally referee results before OpenAI cites them as discoveries, is the structural answer to that gap, and its first ETH report will set the precedent for everything that follows.

What to watch

Three checkpoints will resolve this. First, the shepherd report: which complexity theorists take the ETH paper, and whether they confirm the Lean formalization captures the standard ETH statement. Second, the constants: even a verified subexponential algorithm has complexity-theoretic value regardless of practicality, but the community will want the hidden exponents and constants characterized. Third, the withdrawal count on the broader corpus: if the same review pass finds more errors in the 722, the model’s unaided reliability estimate falls, and the shepherding layer becomes not just a formality but the actual product. The honest summary: a frontier lab claims its model did foundational mathematics, filed the evidence in public, built a verification process, and asked to be checked. That is exactly how extraordinary claims should arrive; what happens next is the part mathematics gets to decide.