cert-machine · the ETH model gap

Anthropic’s ETH proof, carried to a standard Turing machine in one Lean

Two AI labs say a 1999 conjecture about how fast computers can solve hard problems is false. Their proofs check. The objection was that each proof runs on a computer of its own lab’s design. For Anthropic’s proof, that objection now has a Lean answer: it reaches the textbook machine.

checkers that accept the chain
6
Lean’s judge, lake comparator --paranoid; nanoda and leanchecker --fresh besides
declarations under the chain
77,276
accepted by nanoda, a kernel written apart from Lean’s
files of Anthropic’s proof
762 of 809
byte-identical after the port; the other 47 edited, each listed
planted wrong variants
0 accepted
of 9 across the chain, C2 and C1
the story in one minute

What happened, and what I did

The claim. The Exponential Time Hypothesis, proposed by Impagliazzo and Paturi in 1999, says that some problems, like 3-SAT, cannot be solved much faster than trying every possibility: the time has to grow exponentially. Hundreds of results in computer science are built on it. In October 2026, OpenAI and Anthropic each published an AI-written proof that it is false, each checked by Lean, a program that verifies mathematical proofs line by line.

The catch. A proof checker only checks the statement it is given. Each lab stated its result about a computer of its own design, reading the input in its own format. Whether that is the computer of the textbooks, the multitape Turing machine every course teaches, was argued in a paragraph, not proved.

What I did. With AI agents, I wrote a Lean proof that Anthropic’s statement implies the hypothesis fails on a standard multitape Turing machine reading ordinary binary input, for every formula. Then I moved Anthropic’s own proof into the same Lean, 762 of its 809 files unchanged, so every step from their proof to the textbook machine is checked in one place. Six proof checkers accepted it, four of them written apart from Lean’s own kernel, and every one of 9 deliberately wrong versions I planted was refused.

What it means. When an AI lab says “machine-checked”, the question is always what was checked. For Anthropic’s claim, the distance between the headline and the checked statement is now one definition wide: that the textbook’s ETH is this formal one. That last step is a reading of a definition, and always will be. The claim, the algorithm and the paper remain Anthropic’s; this page checks the link, not the mathematics behind it.

The limits come next, then the picture, then every step with its record. The full argument is in the technical note (PDF).

what stays open

What this does not settle

the picture

From each lab’s statement to a standard machine

decided
exact arithmetic backs it
computed
float, or a number someone printed; nothing decided it
OpenAI’s environmentLean v4.34.1 · Mathlib d13f23b7exact_count_and_satOpenAI’s statementHawkleyCERTIFIEDKNETHIsFalsevendored, same bytesseam 1: readAnthropic’s environmentLean v4.33.1 · Mathlib 0df444a3complexitylib’s environmentLean v4.36.0-rc2 · cslib, Mathlib through its pinsthe second seam: crossed by proof, Anthropic’s proof rebuilt hereC Lean’s judge (6 checkers) · K Lean’s kernel · N nanoda · L leanchecker --fresh — ticks where the record acceptedETHIsFalseAnthropic’s statementETHIsFalsesame bytes, proved hereAnthropic’s proofported, 47/809 editedchainCERTIFIEDCKNLcomplexitylib’s proofnative, @ 1b7d62a8¬ ETHcslib multitape TM, encCNF¬ ETHword RAM, O(log L) wordsCERTIFIEDKNLD1CERTIFIEDCKNLC1CERTIFIEDCKNLC2ETH is falsethe textbook statementa reading of a definition, and always one
The chain toward a standard machine, as on /eth/. Solid edges are Lean implications decided here, ticked by the checks their records say accepted (C Lean’s judge with six checkers, K Lean’s kernel, N nanoda, L leanchecker --fresh); a dashed box is a copy read across a version seam; the dashed links to the textbook statement are readings.Records: certs/eth-hawkley-bridge.json · sha256 8d00cca0cdc5; certs/eth-hawkley-heavy.json · sha256 7c88e9465fd4; certs/eth-cslib-d1.json · sha256 73f02f389c22; certs/eth-c1.json · sha256 5252012570a3; certs/eth-c2.json · sha256 71031dd48fae; certs/eth-chain.json · sha256 a6291d9300aa; certs/eth-comparator.json · sha256 be2d801372c4The build refuses this figure if a record it was drawn from has moved since apps/eth/build.js drew it, or any link’s word is not CERTIFIED.
the definition

Where the chain ends, read against the textbook

The port cannot change what the theorem says. The final statement, ¬ETH, mentions only complexitylib’s and cslib’s definitions: the library’s own audit (#check_abstract, run at every build) admits nothing beyond its encoding module into them, and Lean’s judge checked that the theorem’s type is the pinned challenge’s, which imports nothing from the port. None of the 47 edited files can change what not_eth means.

That definition, clause by clause, against Impagliazzo and Paturi (2001). This column is a reading, not a decision; only the time bound needs the judgment of the people who wrote the definition.

clausethe standard ETHcomplexitylib’s ETHour reading
Statements₃ > 0: some δ > 0 admits no O(2^{δn}) algorithm for 3-SAT∃ δ > 0, ¬ DecidableInExpTime (KSAT 3) encCNF numVars δsame
Quantifiers in ¬ETHfor every δ > 0, some algorithmfor every δ, some e, c and one machine, all fixed before the inputs; they may depend on δsame
Machinea deterministic Turing machinecslib's deterministic binary multitape TM: finitely many states, a fixed number of work tapes, a read-only input tape; time counts transitionssame
Problem3-SAT, a decision problemKSAT 3: satisfiable formulas whose clauses have at most 3 literalssame
nthe number of variablesnumVars: the distinct variables occurring, not the largest labelsame
Time bound2^{δn}, polynomial factors implicitc · 2^{δn} · (L+1)^e + c, with L the encoded lengthto confirm: formulas may repeat clauses, so L is not bounded by a polynomial in n and the factor in L is needed; the usual convention, for the definition's authors to confirm
Encodingany reasonable encoding (Garey–Johnson)binary labels with explicit framing; the length proved exactly (length_encCNF: one bit per clause plus 10 + 8·b bits per literal, b the label's binary length)same
Spaceunconstrainedsome space bound must exist; otherwise unconstrainedsame
Inputs that are not encodingsnot addressedno condition, not even on timethe standard promise
  • ETH only, not SETH. The same file also states ¬SETH and that the SAT exponent is 0 for every clause width; complexitylib’s own proof (D1) proves those. The chain from Anthropic’s statement decides ¬ETH only.
  • Who wrote the target. The definition was written by OpenAI, Samuel Schlesinger and Anton Kovsharov, in a library built largely by AI agents and audited by #check_abstract. It is a neutral, checked library, but a reader judging independence should know that the target was co-written by OpenAI.
  • Two complexitylib commits. D1 decided complexitylib at 1b7d62a8; the bridge builds on 7c66eb71, a later commit. The first is an ancestor of the second, both pin the same Lean, cslib and Mathlib, and the files that define the statement are byte-identical between them.
check it yourself

How to check this yourself

contact

Write to Carlos

Sent by Web3Forms to Carlos’s inbox; nothing stored here.

Or write to carlos@carlostoledo.co, or open the public pilot form on GitHub.