---
id: "lib-2026-10-26-exponential-time-hypothesis-refuted-by-ai-models"
type: "library"
title: "Exponential Time Hypothesis refuted by AI models (Anthropic paper and Lean formalization)"
lang: "EN"
org: "Anthropic; OpenAI"
source_type: "Other"
date: "2026-10-26"
week: "2026-W44"
url: "https://nosov.ai/library/lib-2026-10-26-exponential-time-hypothesis-refuted-by-ai-models/"
original_url: "https://github.com/anthropics/formal-math/tree/main/eth"
tier: "S"
tier_name: "Shapes the field"
tier_reason: "An Anthropic paper, with a machine-checked Lean 4 proof, reporting that an internal model refuted the Exponential Time Hypothesis, a standard hardness assumption in complexity theory, with an independent concurrent claim from OpenAI; if it holds, it removes the foundation of hundreds of published results."
summary_basis: "full-text"
original_minutes: "120"
tags: ["ai technology", "ai for science", "formal verification", "mathematics"]
frames: ["verification-capacity"]
---

# Exponential Time Hypothesis refuted by AI models (Anthropic paper and Lean formalization)

Tier S (Shapes the field): An Anthropic paper, with a machine-checked Lean 4 proof, reporting that an internal model refuted the Exponential Time Hypothesis, a standard hardness assumption in complexity theory, with an independent concurrent claim from OpenAI; if it holds, it removes the foundation of hundreds of published results.

Summary based on the full text.

## In short

A paper dated 26 October 2026, credited to Claude (Anthropic), titled "A 2^o(n) time algorithm for 3-SAT". It presents a deterministic algorithm that counts the satisfying assignments of a 3-SAT formula in subexponential time, which refutes the Exponential Time Hypothesis (ETH) of Impagliazzo and Paturi and, with it, the Strong ETH. An internal Claude research model found the core algorithm on 16 October with no human input; Anthropic researchers worked with the model on presentation. The main results are stated and proved in Lean 4. OpenAI separately claims a similar result from its own internal model. The result has no practical use for solving formulas.

## Key numbers

- 14M: output tokens the internal Claude research model used to find the core algorithm, with no human input
- October 16: date the core algorithm was found
- 800: papers found that prove at least one result only under ETH or a hypothesis implying it (more than 800)
- 1,050: Lean modules in the formal development, built from nothing and kernel-checked
- 100: variables at which brute force is already impractical; the new bound beats brute force only at astronomically larger sizes

## What it reports

- Main theorem: #k-SAT on n variables and m clauses is solvable in time 2^O(min{k²n log log n/√log n, km/√log m}), using tensor networks and rank arguments plus count-preserving sparsification.
- Prior records for deterministic 3-SAT were exponential, O(1.328^n); the new bound is subexponential.
- Consequences include subexponential algorithms for Independent Set, Clique, Vertex Cover and Dominating Set, and a circuit lower bound for E^NP. The Orthogonal Vectors hypothesis, on which many fine-grained lower bounds rest, is not refuted.
- A literature search by Claude found more than 800 papers with at least one result proved only under ETH or a stronger hypothesis.
- The result is asymptotic. For 3-CNF formulas with 5n clauses the bound beats exhaustive search only when n exceeds 10^10,000, and the bound in n alone only above 10^(10^8). Brute force is already impractical at 100 variables.
- The Lean development (1,050 modules) is accepted by Lean's kernel, its replay checker and an independent kernel, and uses no axioms beyond Lean's three standard ones.

## How they got it

The model produced the algorithm and proof; the paper gives a weaker theorem in the main body to explain the ideas and proves the full theorem in appendices. The formal statements are given as a definitions-only Lean file, and the full proof and build instructions are public on GitHub.

## Limits

- The Lean development was written by AI models and reviewed by other instances of the same models; at the time of writing no person was known to have checked it.
- Machines check the proof, not whether the two Lean definitions say what ETH and the main theorem mean; the paper leaves that judgement to readers.
- The constant in the bound is not explicit.
- The OpenAI claim is cited, not examined in this paper.
- No peer review yet.

## Why it matters for companies

There is no direct operational effect: the algorithm is useless at any real problem size. The signal is about capability. A model working without human input settled a decades-old open question in theoretical computer science, and the proof was verified by machine rather than by trust. For firms, the practical lesson is the verification pattern: pair model output with an independent checker that can reject it, and treat "reviewed by the same model family" as a gap to close, not as assurance.

Original: https://github.com/anthropics/formal-math/tree/main/eth