Two AI Labs Claim Proofs That the Exponential Time Hypothesis Is False

OpenAI and Anthropic each say an AI disproved the Exponential Time Hypothesis, a 1999 guess about how hard logic puzzles are, about six hours apart. Lean accepts both proofs, but the experts reviewing OpenAI’s say their involvement is not certification.
artificial-intelligence
Author

Kabui, Charles

Published

2026-11-09

Keywords

exponential-time-hypothesis, 3-sat, lean-proof, ai-mathematics, computational-complexity

Download as PDF

The Exponential Time Hypothesis (ETH) is a 1999 guess about a famous logic puzzle, 3-SAT: can yes-or-no variables, linked in groups of three, be set to satisfy every group? ETH says no method is much faster than trying every setting, and OpenAI says hundreds of papers assume it. On October 26, OpenAI announced that its system disproved ETH, with a proof checked in Lean, software that verifies proofs line by line. About six hours after OpenAI’s files went online, Anthropic posted its own paper by Claude, “A 2^o(n) Time Algorithm for 3-SAT”, with its own Lean proof.

Anthropic’s notes say its result “says nothing about solving formulas in practice.” Fabio Dias and Yvens Lima calculate that, for formulas with a fixed number of clauses per variable, OpenAI’s guaranteed running time beats trying every setting only above 2^1,000,000,000 variables and clauses, a number with about 300 million digits. No real formula is that large. Lean also checks a proof only against the statement it is given, and Anthropic’s notes say no machine checks that statement against the paper.

The three experts examining OpenAI’s proof, Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, wrote that their involvement “should not be taken as certification of the claim.” Lance Fortnow has not verified it but says it is “safe to assume” ETH is “toast.” OpenAI claims a proof of the Kakeya conjecture, released without a review group. Three commenters on the review group’s blog say they re-ran both Lean proofs and Lean accepted them.

Read More: what a Lean check does and does not cover, in an earlier OpenAI proof and an earlier OpenAI disproof that nine mathematicians checked in a companion paper

Sources:

Disclaimer: For information only. Accuracy or completeness not guaranteed. Illegal use prohibited. Not professional advice or solicitation. Read more: /terms-of-service

Reuse

GNU GENERAL PUBLIC LICENSE v3.0(View License)

Citation

BibTeX citation:
@misc{kabui2026,
  author = {{Kabui, Charles}},
  title = {Two {AI} {Labs} {Claim} {Proofs} {That} the {Exponential}
    {Time} {Hypothesis} {Is} {False}},
  date = {2026-11-09},
  url = {https://toknow.ai/posts/openai-anthropic-exponential-time-hypothesis-false-3-sat-lean/},
  langid = {en-GB}
}
For attribution, please cite this work as:
Kabui, Charles. 2026. “Two AI Labs Claim Proofs That the Exponential Time Hypothesis Is False.” https://toknow.ai/posts/openai-anthropic-exponential-time-hypothesis-false-3-sat-lean/.