Two Labs’ Claimed Refutations of the Exponential Time Hypothesis Turn Verification Into a Statement-Reading Problem, and Their Lean Theorems Promise Only That a Constant Exists

On October 26, OpenAI published a manuscript and Lean files claiming a refutation of the Exponential Time Hypothesis (ETH), and about six hours later Anthropic published its own paper and Lean project making the same claim. TechCrunch’s explainer, published on October 27, adds that the labs “maybe opened up a path for algorithms that generally perform P = NP.” I read the abstracts, introductions and statements of both papers, both Lean statement files, Anthropic’s public build record and the open letter from the researchers organizing the review, and I checked TechCrunch’s piece against them.

Most of TechCrunch’s account holds up against the documents. The documents also say more, and less, than the headline version:

• The papers are narrower than the press version. Anthropic’s paper says its result “does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems,” and that the bound it proves does not beat exhaustive search unless a formula has more than 10^10,000 variables (3-CNF with five clauses per variable). OpenAI’s post says that turning the advance into practical improvements “will require significant further research.”
• “Verified in Lean” covers the proof, not the statement. Anthropic’s paper says that whether its two main Lean definitions say what they are meant to say is something “no machine can check,” and that “no person is known to have checked” its AI-written Lean development. The build record I could read passed, and a read-only scan I ran found no sorry and no added axiom outside the challenge file.
• The two Lean results differ in scope. Anthropic’s covers its paper’s full printed bound and states “ETH is false” as a Lean proposition. OpenAI’s Lean theorem covers a weaker exponent than its manuscript, and none of the 678 challenge files in its repository listing is named for ETH. Anthropic’s Comparator configuration turns on a second, independently written proof kernel; OpenAI’s configuration for this result turns it off.
• Neither Lean theorem fixes a constant. Both promise only that constants exist, so the practical threshold rests on a calculation in Anthropic’s paper that is human-checked text, not machine-checked Lean.
• The review has barely started. The three researchers organizing it, Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, wrote that “our involvement should not be taken as certification of the claim.”

I did not build either Lean project. Anthropic’s README says its build took about 8 minutes on 24 virtual CPUs with a largest process of about 7 GB, and building any downloaded project runs its code, so I read the public record instead. Nothing here is a judgment on whether either proof is correct. Figures marked as mine are my own arithmetic. For earlier coverage of the same pattern, see our post on OpenAI’s Navier-Stokes claim and the advisory group OpenAI formed for its mathematics claims.

What the two labs claim, and when

ETH is a conjecture about 3-SAT, the problem of deciding whether a Boolean formula made of clauses with at most three literals has a satisfying assignment. Anthropic’s paper introduces it right after P ≠ NP, as “an even stronger conjecture”: that some constant δ > 0 makes it impossible to solve 3-SAT on n variables in time O(2^δn). Refuting it needs, for every δ > 0, an algorithm that runs in time O(2^δn), which any 2^o(n) algorithm provides. Both labs describe a deterministic algorithm that does more than decide satisfiability: it counts the satisfying assignments exactly.

The exponents have the same shape, and both papers tie the sharp bound to tensor methods: Anthropic’s keywords end with “tensor networks, rank,” and OpenAI’s manuscript says its Appendix D proves both bounds “by tensor contraction.” Anthropic’s paper says the core algorithm “was found on October 16 by an internal Claude research model with 14M output tokens and no human input,” and that “independently and concurrently, an internal model at OpenAI claims to have proven a similar result.” The two repositories’ commit times are 6 hours 15 minutes apart. Two groups reaching matching exponents within a day of each other gives reviewers two separate write-ups to compare. It does not, by itself, show that either is right.

What the claims do not say

It is not a proof that P = NP

A bound such as 2^{O(n/√log n)} for sparse formulas grows faster than any polynomial, so a correct result would not by itself put 3-SAT in polynomial time, and neither paper claims it would. Anthropic’s says so in one sentence: “However, our result does not bear on the P vs NP question directly, nor does it yield any practical algorithms for NP-complete problems.” I found no discussion of P versus NP in OpenAI’s manuscript text. Williams’s remark to TechCrunch is a judgment about plausibility, not a claim from either paper: every computer scientist “should probably put a little more weight on the plausibility of P = NP, but one’s weight may vary.” The sentence about a “path” to P = NP is the one that goes beyond the sources.

It is not a faster solver

Anthropic’s paper is blunt: “Our result is purely asymptotic.” For 3-CNF formulas with m = 5n clauses, it says, the bound it proves does not improve on the 2ⁿ of exhaustive search unless n > 10^10,000, and the bound in n alone, which holds for any number of clauses, does not unless n exceeds 10 raised to the power 100,000,000. It adds that its approach seems unlikely to give any general improvement below about 10⁷ variables however it is instantiated, and that “brute force enumeration is already impractical for n = 100, so the improvement of our result does not appear in practical settings.”

To put the first threshold on a human scale, this is my arithmetic: how many bits it would take just to write down a 3-CNF formula with 10^10,000 variables and five clauses per variable.

# scale.py: how big is a formula at the crossover Anthropic's paper states for m = 5n clauses?
import math

log10_n = 10_000  # the paper: the bound beats 2**n only for n > 10**10000 variables
bits_per_index = log10_n * math.log2(10)  # bits needed to name one of n variables
log10_bits = log10_n + math.log10(5 * 3 * bits_per_index)  # 5n clauses x 3 literals x bits each
log10_atoms = 80  # about 10**80 atoms in the observable universe (Eddington number)

print(f"bits to name one variable: {bits_per_index:,.0f}")
print(f"formula size: about 10**{log10_bits:,.1f} bits")
print(f"one bit per atom in the observable universe covers 10**{log10_atoms - log10_bits:,.1f} of it")

It prints:

bits to name one variable: 33,219
formula size: about 10**10,005.7 bits
one bit per atom in the observable universe covers 10**-9,925.7 of it

The formula at the crossover would need about 10^10,006 bits. The observable universe holds roughly 10⁸⁰ atoms (the estimate known as the Eddington number), so even one bit per atom falls short by a factor of about 10^9,926. At the crossover sizes the paper states, the proved bound is no better than exhaustive search, and no formula of that size could ever be written down. OpenAI’s post is more guarded than blunt: “Finding such algorithms, and turning theoretical advances into practical improvements, will require significant further research.”

It is not a reported break of cryptography

Williams told TechCrunch that an improved algorithm could imply that cryptographic systems relying on certain key sizes would be considered broken, so one of his first questions to OpenAI science lead Dan Roberts was whether they had checked. Williams’s account of the answer: “Apparently, they checked, and they were reasonably confident that this didn’t … imply any breaks.” I have not evaluated any cryptosystem. What the papers allow me to say is narrower: a formula an attacker could actually build has far fewer than the 10⁷ variables below which Anthropic says its approach seems unlikely to help in general.

What would change if the result stands

Anthropic’s paper lists consequences that follow with prior work: Independent Set, Clique, Vertex Cover and Dominating Set on graphs with n vertices would be solvable in time O(2^δn) for every δ > 0, and the complexity class E^NP would have no linear-size Boolean circuits. SETH, the stronger hypothesis about k-SAT, falls too, because it is known to imply ETH. The Orthogonal Vectors hypothesis does not fall: the paper says Theorem 1 does not refute it, and “many lower bounds in fine-grained complexity rest” on it, so those are not touched by this claim. On how much literature leans on ETH, the paper says: “In a literature search carried out by Claude, we found more than 800 papers that prove at least one result of their own only under ETH or under a hypothesis that implies it.” That count is a model-generated search I could not reproduce; OpenAI’s post gives a rounder figure, saying ETH “has been used in hundreds of papers.” Williams also told TechCrunch, of the algorithm itself: “I don’t think that OpenAI’s algorithm could possibly be the best algorithm you can get.”

What “verified in Lean” covers

Two separate checks sit behind the phrase. A proof checker confirms that the proof establishes a formal statement. A person confirms that the formal statement means what the headline says. Lean does the first. The second is the part the earlier OpenAI math releases left open too, and the two ETH releases make it unusually easy to inspect because the statements are short and public.

Layer one: the proof

Anthropic’s repository is organized so the first check is mechanical. Its README gives three commands, lake exe cache get, lake build and lake env lean scripts/PrintAxioms.lean, and the output they should print: that both main theorems depend only on Lean’s three standard axioms, propext, Classical.choice and Quot.sound. Its Appendix E says the proofs are accepted by Lean’s kernel, by Lean’s replay checker, and, through Comparator, by the independently implemented kernel nanoda.

The public record agrees. The GitHub Actions run for the release commit, 16a5ce4, shows a job named “verify (eth)” that finished successfully in 24 minutes: the step “lake build (no sorry outside the comparator challenge files)” took 16 minutes, and “Palomar bar (comparator accepts every declared configuration)” took 4 minutes 44 seconds. A read-only scan of the pinned commit adds a cheap sanity check. The script reads the archive in memory and runs nothing from it:

# scan_lean.py: read-only scan of one Lean project folder inside a GitHub tarball.
# The archive is read in memory; nothing is extracted, built or run.
import io
import re
import sys
import tarfile
import urllib.request

repo, sha, folder = sys.argv[1:4]  # for example: anthropics/formal-math 16a5ce41... eth/
url = f"https://codeload.github.com/{repo}/tar.gz/{sha}"
request = urllib.request.Request(url, headers={"User-Agent": "lean-scan-script"})
archive = tarfile.open(fileobj=io.BytesIO(urllib.request.urlopen(request, timeout=180).read()), mode="r:gz")


def code_only(src):
    """Remove Lean comments (line, nested block, doc) and string literals; keep the line breaks."""
    out, i, depth = [], 0, 0
    while i < len(src):
        two = src[i:i + 2]
        if depth:
            if two == "/-":
                depth += 1
                i += 2
            elif two == "-/":
                depth -= 1
                i += 2
            else:
                out.append("\n" if src[i] == "\n" else "")
                i += 1
        elif two == "/-":
            depth = 1
            i += 2
        elif two == "--":
            while i < len(src) and src[i] != "\n":
                i += 1
        elif src[i] == '"':
            i += 1
            while i < len(src) and src[i] != '"':
                i += 2 if src[i] == "\\" else 1
            i += 1
        else:
            out.append(src[i])
            i += 1
    return "".join(out)


WORDS = ["sorry", "axiom", "native_decide", "ofReduceBool", "unsafe", "implemented_by", "extern", "opaque", "theorem", "def"]
totals = {w: 0 for w in WORDS}
where = {w: {} for w in WORDS}
files = size = code_lines = 0
sizes = {}
for member in archive:
    name = member.name.split("/", 1)[-1]
    if not (member.isfile() and name.startswith(folder) and name.endswith(".lean")):
        continue
    text = archive.extractfile(member).read().decode("utf-8", errors="replace")
    code = code_only(text)
    files += 1
    sizes[name] = len(text.encode("utf-8"))
    size += sizes[name]
    code_lines += sum(1 for line in code.split("\n") if line.strip())
    for w in WORDS:
        n = len(re.findall(r"(?<![\w.])" + w + r"(?!\w)", code))
        if n:
            totals[w] += n
            where[w][name] = n

print(f"Lean files: {files}, {size:,} bytes, {code_lines:,} non-blank code lines outside comments")
print(f"theorem keywords: {totals['theorem']:,}   def keywords: {totals['def']:,}")
for w in WORDS[:8]:
    print(f"{w}: {totals[w]}", where[w] if where[w] else "")
statement = folder + "MainResults.lean"
print(f"{statement}: {sizes[statement]:,} bytes = {100 * sizes[statement] / size:.3f}% of all Lean bytes")

Run as python -I scan_lean.py anthropics/formal-math 16a5ce41304fcdaea4e0be7c132e1c361dc26da5 eth/, it prints:

Lean files: 1052, 8,223,990 bytes, 92,396 non-blank code lines outside comments
theorem keywords: 8,267   def keywords: 3,330
sorry: 2 {'eth/Challenge.lean': 2}
axiom: 0 
native_decide: 0 
ofReduceBool: 0 
unsafe: 0 
implemented_by: 0 
extern: 0 
opaque: 0 
eth/MainResults.lean: 11,542 bytes = 0.140% of all Lean bytes

The two sorry placeholders are the ones the README says to expect in Challenge.lean, which states the two theorems without proofs for the Comparator run. Outside comments and strings, nothing in the 1,052 files declares an axiom or uses native_decide. That is a token scan, not a proof of soundness; the axiom printout and the Comparator run are the real checks.

OpenAI’s repository is built differently. Its post says the result “was subsequently verified in Lean,” and GitHub’s tree listing, which was truncated, shows at least 3,978 Lean files totalling about 35.5 MB under paths containing SubexponentialSAT. The repository’s workflows folder holds one file, lock-prs.yml, so there is no public build log of the Lean check for me to read, and the Comparator configuration for this result sets enable_nanoda to false. That does not mean the proof would fail a second kernel. It means that, from outside, the check is something a reader must run, not something I could see run.

Layer two: the statement, read the way the README asks

Anthropic makes the second check short on purpose. MainResults.lean is 11,542 bytes, 0.14 percent of the folder’s Lean source by size, contains definitions only, and imports nothing but Mathlib. The README is plain about the limit: “Lean checks the proofs, but no machine checks that this file says what the paper says; the file is kept short so that a reader can check this.” The definitions that carry the claim are these, with the docstrings left out:

def InTime (k : ℕ) (δ : ℝ≥0) : Prop :=
  ∃ (M : TM2ComputableAux Bool Bool) (c : ℕ), (∀ i, Finite (M.tm.Γ i)) ∧
    DecidesKSat k M fun n => ⌊(c : ℝ) * (2 : ℝ) ^ ((δ : ℝ) * n)⌋₊

noncomputable def s (k : ℕ) : ℝ≥0∞ := ⨅ (δ : ℝ≥0) (_ : InTime k δ), (δ : ℝ≥0∞)

def ETH : Prop := 0 < s 3

def ETHIsFalse : Prop := ¬ ETH

def MainTheorem : Prop :=
  ∃ (M : TM2ComputableAux Bool Bool) (C : ℕ), (∀ i, Finite (M.tm.Γ i)) ∧
    ∀ (k n : ℕ) (φ : CNF n), 1 ≤ k → IsKCNF k φ → 2 ≤ φ.length → 4 ≤ n → AllOccur φ →
      CountsWithin M k φ (timeMin C k φ.length n)

Read in words, with the file’s own comments as the guide:

• The machine. An algorithm is a Mathlib Turing.FinTM2, “a deterministic machine with finitely many stacks in place of tapes,” with finite alphabets, and time is the number of steps.
• The input. The number of variables in unary, then a fixed-width field for each of the k positions of each clause. A clause is a list of at most k literals and no clause is written twice, so “a k-CNF on n variables has at most (2n+1)^k clauses.”
• What ETH is. s k is the infimum of the exponents δ for which some machine decides k-SAT within c·2^δn steps. ETH says s 3 is positive and ETHIsFalse says it is not, which the docstring spells out as: for every δ > 0 some deterministic algorithm decides 3-SAT in time O(2^δn).
• The bridge to ordinary algorithms. A comment argues that a random-access machine simulates such a stack machine with bounded overhead, then says: “The simulation and the rewriting are standard facts; they are not part of the Lean statements or proofs.” The step is standard, and it is also exactly the kind of step a statement reader has to accept on the authors’ word.
• The corner cases. MainTheorem requires at least two clauses, at least four variables, and every variable occurring. At m = 1 the divisor √(log m) is 0, and “Lean’s convention x/0 = 0 would make the bound one step there too.” The docstring says nothing is claimed for other inputs.

Two more facts bear on how far to trust the statement. The constant C is existentially quantified, so the theorem says a constant exists and nothing about its size; the paper agrees: its constant “is not explicit.” And the paper’s own account of what remains unchecked is unusually direct. Appendix E says that whether the two definitions say what they are meant to say is something “no machine can check,” that “that is for the reader of the listing to judge,” and that the Lean development “was written by AI models and reviewed by other instances of the same models; at the time of writing no person is known to have checked it.”

OpenAI’s statement reads differently

OpenAI’s Comparator challenge, SubexponentialSAT.lean (7,833 bytes), states one theorem for each fixed k ≥ 2 over its own machine and formula definitions. These are its quantifiers and its time bound, with the middle of the statement left out:

noncomputable def runtimeScale (n : ℕ) : ℝ :=
  (n : ℝ) * (Real.log (Real.log ((n : ℝ) + 16))) ^ 2 /
    Real.sqrt (Real.log ((n : ℝ) + 16))

noncomputable def runtimeBound (constant exponentConstant : ℝ)
    (degree inputBits numVars : ℕ) : ℝ :=
  constant * ((inputBits : ℝ) + 1) ^ degree *
    (2 : ℝ) ^ (exponentConstant * runtimeScale numVars)

theorem exact_count_and_sat (k : ℕ) (hk : 2 ≤ k) :
    ∃ (machine : Computation.PrimitiveMachine)
      (countTape answerTape : Fin machine.tapeCount)
      (C A S : ℝ) (d e : ℕ),
      0 < C ∧ 0 < A ∧ 0 < S ∧ 0 < d ∧ 0 < e ∧
      ∀ (n : ℕ) (F : SAT.CNF (Fin n)), SAT.WidthAtMost k F →
        -- (the run, the output tapes and the answer are left out here)
          (time : ℝ) ≤ OAI.Algorithms.SubexponentialSAT.SqrtLog.Statement.runtimeBound C A d
            (Encoding.formulaBitLength F) n ∧
        -- (the space bound, in the same style, follows)
              S * ((Encoding.formulaBitLength F : ℝ) + 1) ^ e

Four differences stand out:

• The exponent. The bound is n·(log log (n+16))²/√log (n+16), the weaker (log log n)² form. OpenAI’s scope note says so: Lean proves that bound, while “the October 25 manuscript gives the sharper time bound,” with a single log log factor and, for sparse formulas, n/√log n. The weaker bound is still enough for ETH, because (log log n)²/√log n tends to 0, but the sharper claims are manuscript-only.
• Space. The theorem also bounds every step of the run to polynomially many visited tape cells, which Anthropic’s statement does not.
• No “ETH is false” statement. The scope note links one Comparator statement, the counting theorem. None of the 678 challenge files in the repository listing has ETH in its name, and the three other SAT files I opened concern random formulas and clause thresholds. The step from the counting theorem to “ETH is false” is made in the manuscript, not in Lean.
• Constants. (C A S : ℝ) (d e : ℕ) are all existential, so no value is pinned down.

Who checks which link

How the review is being organized

The open letter signed by Impagliazzo and Paturi (UC San Diego) and Williams (MIT) starts: “OpenAI has informed us that it has obtained a claimed refutation of the Exponential Time Hypothesis and plans to release the supporting documents to the community.” It continues, “Our involvement should not be taken as certification of the claim,” and adds that “if the claim is correct, it will change an important part of theoretical computer science.” Its resource list points to OpenAI’s release, a community repository the three maintain, a response form, a discussion blog and Anthropic’s refutation, and it floats “a proposed virtual meeting before the end of 2026.”

OpenAI’s post describes the same arrangement from its side: “Participants will not be asked to sign nondisclosure agreements,” OpenAI says it does “not seek academic credit for the discoveries produced by our internal models,” and it has agreed to fund a conference. It calls the manuscripts “a form of raw research data.” Its repository README goes further: “We defer to the math community completely on matters of credit, precedence, and concurrent work.” Anthropic’s README is terser: “Research artifact. Not maintained and not accepting contributions.” It also carries a condensed description of the key idea “interpretable by AI models,” and says Claude Opus 5.5 at high effort “can rederive the refutation of ETH” from it. I did not test that claim.

Williams’s view, as TechCrunch reports it, is mixed. Some parts of OpenAI’s proof are routine, but “there are two or three alien-looking parts,” and “this is something that the whole community needs to work on together.”

One detail in TechCrunch’s chronology needs care. It says Anthropic mathematician Levent Alpöge “suggested that OpenAI was basing its solutions on pre-existing work,” and that Anthropic released its refutation hours later. The post TechCrunch links, from October 26 at 21:54 UTC, is about OpenAI’s physics release: it says a researcher, Ethan Sussman, had been publicly writing up existence results he labels YM4, QED3 and YM3, and it faults OpenAI for not contacting him. It does not mention ETH. I take no position on that dispute, and it is not evidence about the ETH result.

A short audit anyone can repeat

You do not need Lean to run most of the check on a claim like this. In order:

1. Read the statement file’s docstrings before its code, then the code. For Anthropic that is one file; for OpenAI it is one challenge file plus the definitions it carries.
2. Open the commit and its build record, and read the step names and conclusions, not only the green mark.
3. Run the scan above against the pinned commit, so the numbers cannot drift with later pushes.
4. Compare the statement with the paper’s printed theorem. Anthropic’s Appendix E prints its statement file and lists how it differs from the paper’s statements; OpenAI’s scope note lists where Lean falls short of the manuscript.
5. Only then, if it matters to you, rebuild in a disposable virtual machine using the README’s three commands.

What to watch next

• A human-written account from the working group of the proof’s “alien-looking parts,” and whether it finds them sound.
• An OpenAI Lean statement of “ETH is false” itself, a Comparator run with the second kernel on, and Lean coverage of the sharper exponent.
• Explicit constants. The thresholds in Anthropic’s paper come from a hand calculation; a Lean statement with explicit constants would let a machine check them.
• The Orthogonal Vectors hypothesis, which Anthropic says this result does not touch, and the lower bounds that rest on it.
• The community meeting the letter proposes for before the end of 2026.

Nothing in this post is a verdict on either proof. It is a reading of what the two labs, the review organizers and TechCrunch have published, and of what could be checked from outside as of the evening of October 27, UTC.