---
title: "Did OpenAI and Anthropic Just Refute the Exponential Time Hypothesis? What the 3-SAT Claims and Lean Proofs Actually Show"
description: "OpenAI and Anthropic claim AI models refuted the Exponential Time Hypothesis for 3-SAT with Lean 4 proofs. Here is what Lean checks and what it cannot."
canonical_url: https://www.oguzhan.co/exponential-time-hypothesis-false-openai-anthropic-3-sat/
author: "Oğuzhan Koçaklı"
author_url: https://www.oguzhan.co/about/
date_published: 2026-10-28T07:22:05+00:00
date_modified: 2026-10-28T07:22:08+00:00
language: en
translations:
  tr: https://www.oguzhan.co/tr/ustel-zaman-hipotezi-eth-openai-anthropic-3-sat/
---

# Did OpenAI and Anthropic Just Refute the Exponential Time Hypothesis? What the 3-SAT Claims and Lean Proofs Actually Show

Two frontier AI labs stepped forward in the same week with the same extraordinary claim: the **Exponential Time Hypothesis (ETH)**, one of theoretical computer science’s load-bearing hardness assumptions, is false. On October 26, 2026, [OpenAI](https://openai.com/index/building-scientific-understanding-with-academic-communities) announced that an internal system had disproved ETH and formalized the proof in Lean, publishing the manuscript in its [`openai/math` repository](https://github.com/openai/math). According to [WebProNews](https://www.webpronews.com/openai-anthropic-exponential-time-hypothesis-refuted-sat/), about six hours separated the two labs’ GitHub commits on October 26 (OpenAI at 4:52 p.m. ET and Anthropic at 11:07 p.m. ET), before [Anthropic](https://github.com/anthropics/formal-math/tree/main/eth) publicly released its own paper and [Hexagon preprint](https://hexagonmath.org/2610.00577v1) on October 27, crediting the paper directly to Claude.

Stranger still, both labs trace the core algorithmic breakthrough to the exact same calendar date: October 16, 2026. Both groups present deterministic subexponential algorithms that count the satisfying assignments of k-CNF formulas, and both attach machine-checked Lean formalizations to back up their claims. Neither paper has undergone traditional peer review yet, so every technical statement from both labs remains an unreviewed claim until human complexity theorists finish inspecting the definitions and reductions. Still, when two competing labs independently drop machine-checked refutations of the same foundational conjecture on the same day, the interesting story is not the breathless social media chatter about P versus NP, which remains untouched, but the mechanics of the proof, the astronomical constants hiding inside the asymptotics, and the very specific gap that even a formal proof assistant cannot close on its own.

## What Is the Exponential Time Hypothesis, and Why Does Anyone Care?

The **Exponential Time Hypothesis (ETH)** is a foundational conjecture in complexity theory proposed by Russell Impagliazzo and Ramamohan Paturi (with Francis Zane) stating that 3-SAT cannot be solved in subexponential time `2^{o(n)}`. If ETH is false, deterministic algorithms can asymptotically beat `c^n` for every constant `c > 1`, overturning conditional lower bounds in more than 800 published papers without settling P versus NP.

To see why complexity theorists immediately stopped what they were doing this week, you have to look at 3-SAT, the canonical boolean satisfiability problem. Given a boolean formula with `n` variables and `m` clauses, where each clause is an OR of at most three literals (a 3-CNF formula, or more generally a k-CNF formula for a fixed clause width `k ≥ 2`), the decision problem asks whether at least one assignment of true and false values makes the entire formula true. Its counting cousin, #3-SAT, asks a harder question: exactly how many of the `2^n` possible assignments satisfy the formula?

Brute force checks all `2^n` assignments. For decades, researchers have shaved down the base of that exponent for deterministic and randomized algorithms without ever escaping an exponent that grows linearly with `n`. As cited in [Anthropic’s paper PDF](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf), the prior deterministic record for 3-SAT stood at `O(1.328^n)` (Liu, 2018), the randomized record along the PPSZ line stood at `O(1.308^n)`, and the prior record for #3-SAT counting stood at `O(1.6423^n)` (Kutzkov, 2007). Every single one of those algorithms still takes `c^n` time for some constant `c > 1`.

Impagliazzo and Paturi conjectured that this barrier is fundamental: 3-SAT requires `2^{Ω(n)}` time, meaning some positive constant in the exponent must always remain. That assumption is much stronger than `P ≠ NP`. Because `P ≠ NP` only says 3-SAT has no polynomial-time `n^{O(1)}` algorithm, computer scientists needed ETH as a sharper ruler to prove fine-grained lower bounds across algorithms and complexity theory.

According to [OpenAI’s October 26 post](https://openai.com/index/building-scientific-understanding-with-academic-communities), ETH “has been used in hundreds of papers” to establish conditional hardness across graph theory, computational biology, databases, and computational geometry. In [Anthropic’s paper](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf), a literature search run by Claude found more than 800 papers that prove at least one theorem only under ETH or a stronger hypothesis that implies it, such as the Strong Exponential Time Hypothesis (SETH) or Gap-ETH. If ETH is genuinely false, the conditional lower bounds in those 800-plus papers lose their foundation at once.

![Tangled copper and teal constraint graph passing through octagonal rings into an ordered golden cubic crystal lattice](https://oguzhanco.s3.eu-west-3.amazonaws.com/wp-content/uploads/2026/10/28071639/3-sat-tensor-network-contraction-octonions.webp)

*At a high level, Anthropic’s paper rewrites 3-SAT counting as a tensor-network contraction and uses an 1840s eight-square identity from the octonions to cancel crossing constraints.*

## What Exactly Did OpenAI and Anthropic Claim?

Both OpenAI and Anthropic claim that internal AI models discovered deterministic subexponential algorithms on October 16, 2026 that count all satisfying assignments of k-CNF formulas for any fixed clause width `k`. OpenAI claims a runtime of `(n+m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}}` in polynomial space, while Anthropic claims a #3-SAT runtime of `2^{O(n log log n / √log n)}` formalized across 1,050 Lean 4 modules.

When I read through both repositories and preprints side by side, the most striking detail was that neither model settled for the decision version of 3-SAT. Both claimed deterministic subexponential algorithms for the harder counting problem across any fixed clause width `k`.

In [OpenAI’s `openai/math` repository](https://github.com/openai/math), where `CONTENTS.md` now lists 721 manuscripts covering 373 result families (expanding on the early October batch we examined in our [analysis of OpenAI’s first 722 math papers and Lean verification](https://www.oguzhan.co/openai-math-results-722-papers-lean-agmai/)), the ETH disproof appears as result 378 under a folder carrying a preprint dated October 25, 2026, titled *“The Exponential Time Hypothesis is False”*. OpenAI’s entry states that for every fixed `k ≥ 2`, a deterministic polynomial-space algorithm counts the satisfying assignments of a k-CNF formula with `n` variables and `m` clauses in time `(n+m)^{O_k(1)} 2^{n/(log n)^{1/2+o(1)}}`.

OpenAI also notes a major complexity-theoretic consequence inside result 378: the algorithm yields superlinear circuit lower bounds for a language in `E^NP` on infinitely many input lengths. And ETH was only one of three headline claims in [OpenAI’s announcement](https://openai.com/index/building-scientific-understanding-with-academic-communities). Alongside computer science, OpenAI reported a proof in mathematics of the local smoothing conjecture in every dimension (which implies both the Kakeya conjecture and Stein’s restriction conjecture in all dimensions, with AI output on October 18 and Lean formalization the next day) and a claim in mathematical physics offering a rigorous existence proof of interacting four-dimensional quantum field theories, including quantum chromodynamics (QCD) and a unified completion of the Standard Model. That physics package includes pure Yang-Mills existence, part of a Clay Millennium Prize problem, where the natural-language proof was produced on September 9, QCD followed on September 18, and the Yang-Mills Lean formalization finished on October 16.

[Anthropic’s repository](https://github.com/anthropics/formal-math/tree/main/eth) and [Hexagon preprint](https://hexagonmath.org/2610.00577v1) (paper dated October 26, deposited October 27) focus entirely on satisfiability under the title *“A `2^{o(n)}` Time Algorithm for 3-SAT”*, authored by Claude (Anthropic). Its Main Theorem covers k-CNF counting for any fixed clause width and solves #3-SAT in deterministic time `2^{O(n log log n / √log n)}`.

How does a deterministic algorithm beat `c^n` without guessing? At a plain-language level, [Anthropic’s paper](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf) rewrites the problem of counting satisfying assignments as a tensor-network contraction, expressing the count as sums of products over a network. Whenever constraints cross in ways that would normally blow up the treewidth, the algorithm replaces those crossing constraints with signed linear combinations that allow algebraic cancellation, picks a tailored grouping for each term, and recurses. The algebraic engine that makes those signed cancellations work without losing count is a classical 1840s result known as Degen’s eight-square identity, which expresses the multiplicative norm of the octonions.

| Dimension | OpenAI | Anthropic |
| --- | --- | --- |
| Published | 26 Oct 2026 (blog + openai/math repo) | 27 Oct 2026 (formal-math repo + Hexagon, paper dated 26 Oct) |
| Model found it | 16 Oct 2026, internal model | 16 Oct 2026, internal Claude research model, 14M output tokens, no human input |
| Claimed bound | counts k-CNF solutions in `(n+m)^{O_k(1)}·2^{n/(log n)^{1/2+o(1)}}` | counts 3-SAT solutions in `2^{O(n log log n/√log n)}`, any fixed k |
| Formal check | Lean, formalized 17 Oct | Lean 4 v4.33.1, second kernel nanoda, 1,050 modules |
| Human review | Impagliazzo, Paturi, Williams group | none known at time of writing (per paper) |
| Extra claim | superlinear circuit lower bounds for a language in E^NP | rederivable by Claude Opus 5.5 from a one-paragraph hint |

![Two tracks converging at a green node, passing three glass verification arches, and stopping at a bridge gap and lens](https://oguzhanco.s3.eu-west-3.amazonaws.com/wp-content/uploads/2026/10/28071641/openai-anthropic-eth-parallel-lean-verification-timeline.webp)

*Both internal models found their core algorithms on October 16 and passed Lean kernel checks, but human complexity theorists still have to inspect the gap between the Lean file and the paper.*

## Does This Mean P = NP, or Faster SAT Solvers Tomorrow?

No on both counts. Refuting the Exponential Time Hypothesis replaces `2^{δn}` with a subexponential bound like `2^{O(n log log n / √log n)}`, which is still far slower than polynomial time `n^{O(1)}`. Furthermore, the hidden constants are so large that the new bound does not beat `2^n` brute force until `n > 10^10` (or `n > 10^10000` for `m = 5n` clauses), leaving real-world SAT solvers unchanged.

First, subexponential time `2^{o(n)}` is still vastly slower than polynomial time `n^{O(1)}`. Replacing `2^{δn}` with `2^{n / √log n}` refutes the Exponential Time Hypothesis, which is why theorems conditioned on ETH, SETH, or Gap-ETH are affected, but it does not put 3-SAT into P. As [Anthropic’s paper](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf) explicitly notes, the result does not settle P versus NP, and it does not even refute the Orthogonal Vectors hypothesis, meaning many fine-grained quadratic-time lower bounds in P that rely on Orthogonal Vectors rather than SETH can still survive on their own footing.

Second, the asymptotics hide constants that only kick in at astronomical input sizes. [Anthropic’s paper](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf) is refreshingly blunt about its own practicality:

- For a 3-CNF formula with `m = 5n` clauses, the paper’s proven bound does not beat naive `2^n` brute force unless the number of variables exceeds `n > 10^10000`.
- Even if you look at the bound in `n` alone, it does not cross below `2^n` until `n > 10^10`.
- The authors add that the general approach is unlikely to yield any improvement at all unless `n > 10^7`, whereas brute force `2^n` is already completely impractical at `n = 100`.

As the paper puts it verbatim: *“Thus our result says nothing about solving formulas in practice.”*

![Long perspective grid hall where cyan and amber light ribbons stay apart and only cross at a distant horizon point](https://oguzhanco.s3.eu-west-3.amazonaws.com/wp-content/uploads/2026/10/28071642/3-sat-subexponential-bound-vs-brute-force-scale.webp)

*The asymptotic bound beats brute force only at astronomical scales: beyond 10^10 variables in n alone, and beyond 10^10000 variables for 3-CNF with m = 5n clauses.*

## What Does Lean Actually Prove, and Where Is the Gap It Cannot Close?

Lean 4 mechanically verifies that a theorem’s proof steps follow logically from the formal definitions written in code, using only standard axioms. However, Lean cannot verify that the top-level formal specification in `MainResults.lean` faithfully matches the informal mathematical claim in the paper without a subtle definitional shortcut or vacuity.

Because [frontier models](https://www.oguzhan.co/what-is-a-frontier-model/) are notorious for writing plausible-sounding mathematical hallucinations, both labs leaned heavily on the Lean theorem prover. In [Anthropic’s `formal-math/eth` repository](https://github.com/anthropics/formal-math/tree/main/eth), the formalization is built on Lean 4 v4.33.1 with Mathlib across 1,050 Lean modules, compiling in roughly 8 minutes on 24 vCPUs and about 7 GB of RAM. The top-level file `MainResults.lean` states both `ETHIsFalse` and `MainTheorem` directly on Mathlib Turing machines. To rule out exploit tricks inside the proof assistant, Anthropic verified that the proofs depend only on Lean’s three standard axioms (`propext`, `Classical.choice`, and `Quot.sound`), ran `leanchecker`, and checked the build through a second, independent kernel called `nanoda` via Comparator.

As we noted in our [weekly roundup on formal verification fences and proofs](https://www.oguzhan.co/ai-weekly-19-25-oct-2026-fences-and-proofs/), checking a proof inside an independent kernel is as strong as mechanical verification gets for internal logical consistency. Once `nanoda` and the Lean kernel accept the proof terms without custom axioms or `sorry` placeholders, the deduction from the stated definitions to the stated theorem is air-tight.

So why is this still framed as a claim rather than an established theorem? Because of the specification boundary. [Anthropic’s README](https://github.com/anthropics/formal-math/tree/main/eth) states the limitation in a single sentence that every computer scientist should memorize:

> “Lean checks the proofs, but no machine checks that this file says what the paper says.”

A formal proof assistant guarantees that `Theorem A` follows from `Definition B`. It cannot guarantee that `Definition B` in `MainResults.lean` faithfully captures what human complexity theorists mean by a deterministic Turing machine running time on a 3-CNF formula without a subtle vacuity, a degenerate encoding, or an unintended shortcut in the cost model. And on that exact point, [Anthropic’s paper](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf) includes a remarkable disclosure: the entire Lean development *“was written by AI models and reviewed by other instances of the same models”* and, at the time of publication, *“no person is known to have checked it.”*

OpenAI took a different operational route to address that exact human bottleneck. In [its October 26 announcement](https://openai.com/index/building-scientific-understanding-with-academic-communities), OpenAI calls its AI-generated manuscripts “raw research data” and introduces external academic “shepherds” who decide how each result should be vetted and released. For mathematics, the shepherds chose to release the AI output directly. For physics, a shepherd group led by David Gross alongside Michael Douglas, Arthur Jaffe, Igor Klebanov, and Nikita Nekrasov chose to hold the raw AI artifacts back while human physicists write up the exposition. For the ETH disproof in computer science, OpenAI turned to the domain’s founding authorities: Russell Impagliazzo (UC San Diego), Ramamohan Paturi (UC San Diego), and Ryan Williams (MIT). Impagliazzo and Paturi are the original proposers of ETH, and Williams is famous for refuting strong variants of ETH-type hypotheses. That group asked that all raw AI data be made public immediately and that OpenAI fund a dedicated conference on the implications, alongside OpenAI’s broader $5 million contribution to the Simons Foundation for workshops on AI-produced science.

## Who Gets the Credit When a Model Finds the Proof?

The two releases also represent a sharp philosophical split on scientific authorship.

[OpenAI](https://openai.com/index/building-scientific-understanding-with-academic-communities) laid out four explicit principles for its academic collaborations: Transparency (no non-disclosure agreements), No Academic Credit (OpenAI explicitly states that it does not seek academic authorship or credit for the raw AI outputs), Recognition (credit belongs to the independent human researchers who verify, interpret, and write up the scientific understanding), and Independence (the shepherds work voluntarily and unpaid). Under OpenAI’s model, the AI output is treated like raw telescope data from an observatory.

[Anthropic](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf) went the opposite way. The PDF lists **Claude (Anthropic)** on the author line. In the provenance note, Anthropic states: *“The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input. Anthropic researchers worked with Claude to improve the presentation.”* The paper also acknowledges the parallel breakthrough across town: *“Independently and concurrently, an internal model at OpenAI claims to have proven a similar result.”*

Even more provocatively, [Anthropic’s Apache 2.0-licensed README](https://github.com/anthropics/formal-math/tree/main/eth) includes a one-paragraph mathematical hint (mentioning the tensor-network formulation and octonion eight-square cancellation) and notes that *“Claude Opus 5.5 at high effort can rederive the refutation of ETH from the following condensed description”*, specifically recovering the basic `O(2^{δn})` bound for every `δ > 0`, though not the sharper `2^{O(n log log n / √log n)}` bound without the full 14-million-token search. When a frontier model can compress a 25-year-old open conjecture into a one-paragraph prompt that another model instance can re-expand into a proof, traditional rules around who discovered what start to buckle.

What happens next comes down to human eyes on formal definitions. Watch for two concrete milestones in the coming weeks: first, the technical report from Impagliazzo, Paturi, and Williams dissecting OpenAI’s result 378 and the upcoming OpenAI-funded workshop on fine-grained complexity, and second, independent Lean experts auditing Anthropic’s `MainResults.lean` and Mathlib Turing machine definitions to confirm that `ETHIsFalse` contains no definitional loophole. If both specifications hold up under human scrutiny, October 16, 2026 will go down as the day two autonomous models quietly broke the backbone of fine-grained complexity theory within hours of each other.

## Frequently Asked Questions

### Did OpenAI and Anthropic prove P = NP?

No. Both labs claim subexponential time algorithms (`2^{o(n)}`) for counting k-CNF satisfying assignments, which is asymptotically faster than `c^n` for any constant `c > 1` and therefore refutes the Exponential Time Hypothesis, but `2^{o(n)}` is still superpolynomial and does not place 3-SAT in P.

### Will these new 3-SAT algorithms make practical SAT solvers faster?

No. According to Anthropic’s paper, the asymptotic bound for 3-CNF with `m = 5n` clauses does not beat naive `2^n` brute force until `n > 10^10000`, and the bound in `n` alone does not beat `2^n` until `n > 10^10`. The paper explicitly states that the result says nothing about solving formulas in practice.

### If the proofs are verified in Lean 4, why are they still called claims?

Lean 4 and the independent kernel `nanoda` verify that the theorem follows logically from the definitions in `MainResults.lean`. However, no machine checks that those formal definitions accurately match the informal problem statement in the paper, and at the time of Anthropic’s release no human had yet audited the 1,050 AI-written Lean modules.

## Sources

- OpenAI (Oct 26, 2026): [Working with academic communities to build scientific understanding](https://openai.com/index/building-scientific-understanding-with-academic-communities)
- OpenAI GitHub Repository: [`openai/math` (Result 378: “The Exponential Time Hypothesis is False”)](https://github.com/openai/math)
- Anthropic GitHub Repository (Oct 27, 2026): [`anthropics/formal-math/tree/main/eth`](https://github.com/anthropics/formal-math/tree/main/eth)
- Claude / Anthropic Paper PDF: [A `2^{o(n)}` Time Algorithm for 3-SAT](https://github.com/anthropics/formal-math/blob/main/eth/paper.pdf)
- Hexagon Preprint (Oct 27, 2026): [`hexagonmath.org/2610.00577v1`](https://hexagonmath.org/2610.00577v1)
- WebProNews (Oct 27, 2026): [OpenAI and Anthropic Refute Exponential Time Hypothesis](https://www.webpronews.com/openai-anthropic-exponential-time-hypothesis-refuted-sat/)