A central assumption about computing time faces a claimed refutation
- What it is
- A manuscript claims an algorithm that counts solutions to fixed-width Boolean formulas in subexponential time and polynomial space.
- Who did it
- OpenAI; an external group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will examine and explain the work.
- What it could mean
- If correct, it would overturn a widely used assumption about worst-case computing time. It does not resolve P versus NP or demonstrate a practical solver improvement.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
The Exponential Time Hypothesis is False ↗See the proposed checks
Inspect the fixed-k quantifiers, canonical encoding and concrete machine endpoint, then compare its time and all-prefix space bounds with the manuscript. Keep the manuscript's single-log-log factor and sparse-clause refinement separate from Lean's squared-log-log factor. Select one bounded correspondence check before any isolated replay; no P=NP or practical speedup follows.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
Structure inside a vast search
The branching tiles introduce the combinations in a Boolean search. The gathered ribbons are a conceptual metaphor, not the submitted algorithm or a measured speedup.
Read the source · Introduction · fixed-width exact counting; lean/docs/378.md · weaker formal runtime ↗- Source kind
- Mathematical research record
- Evidence reported
- Manuscript; independent examination not started
- Source date
- ; added 2026-10-26
- What it claims
- For fixed k≥2, the manuscript claims exact counting on n-variable, m-clause k-CNF formulas in (n+m)^Ok(1) times 2^Ok(n log log n / sqrt(log n)), using polynomial space; for m≤Dn with fixed D, the exponent improves to O(k,D)(n / sqrt(log n)). The public Lean scope instead gives the weaker exponent Ok(n (log log n)² / sqrt(log n)) with a polynomial canonical-input-length factor, still subexponential.
- Why this could matter
- A central assumption about computing time faces a claimed refutation Many conditional speed limits assume that solving three-variable Boolean clauses needs exponentially growing time. The claimed algorithm grows more slowly asymptotically and also counts solutions. The public formalization advertises a weaker time bound than the manuscript.
- If it holds up
- Researchers would revisit hardness claims that depend on ETH and investigate which algorithmic ideas yield useful improvements on actual workloads.
- If it does not
- A failed reduction, time bound or formal correspondence would identify the gap; it would not prove ETH true.
- Impact horizon
- Foundational · Computational complexity · Exact counting · Algorithms
- Version
- 2026-10-25; October 17 manuscript, revised October 25, 2026; public release at Git commit 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a.
- Why we tracked it
- source-reviewed intake only; independent examination has not started.
- Highest-risk dependency
- Analyst judgment: the precise fixed-width encoding, machine-cost model, reduction overhead and manuscript-to-Lean correspondence are load-bearing. Lean's advertised exponent has (log log n)²; the sharper prose bound has log log n, with an additional sparse-case improvement. A replay of the weaker endpoint would not by itself certify those sharper bounds. This is source intake only, not proof validation, polynomial-time SAT or demonstrated commercial acceleration.
- Available artifacts
- Pinned openai/math 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a; paper.pdf (Git blob 0503566e95bc587a4076573a45132d97531b8ba6), lean/docs/378.md, lean/OAI/Algorithms/SubexponentialSAT/SqrtLogSpace/Final.lean and lean/ComparatorChallenges/SubexponentialSAT.json. Lean v4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. The comparator permits the three listed standard axioms and disables nanoda. No State of Proof build or checker run occurred.
- Current boundary
- Intake record only; examination not started. State of Proof has only recorded this intake. The paper's full argument remains unexamined; the next bounded check is: Inspect the fixed-k quantifiers, canonical encoding and concrete machine endpoint, then compare its time and all-prefix space bounds with the manuscript. Keep the manuscript's single-log-log factor and sparse-clause refinement separate from Lean's squared-log-log factor. Select one bounded correspondence check before any isolated replay; no P=NP or practical speedup follows.