OpenAI and Anthropic each published a Lean proof meant to show that ETH is false. Here both proofs were replayed from their pinned bytes, and two kernels accepted each one against its own statement. A kernel cannot say what a statement means. Whether each statement says “ETH is false” was read by two independent readers, and the page keeps the two kinds of check apart.
| claim | toolchain | theorems | verdict | axioms | nanoda |
|---|---|---|---|---|---|
| openai/math @ 7ef5c0cc | Lean v4.34.1 | exact_count_and_sat | CERTIFIED | the three standard | off as shipped; switched on here |
| anthropics/formal-math @ 16a5ce41 | Lean v4.33.1 | ethIsFalse mainTheorem | CERTIFIED | the three standard | on, as shipped |
What CERTIFIED means here. Comparator exit 0 with "Your solution is okay!", Lean's kernel and nanoda both accept, and #print axioms (our file) names only propext, Classical.choice, Quot.sound for every main theorem. It does not mean that a Lean statement is its paper’s theorem, nor that ETH is false. No machine checks that, and both claimants say so.
What was changed, and declared before the run.
Not run: leanchecker --fresh, an optional third replay, on either claim. The machine was deleted after the two kernels had decided, because it was billing unattended (corpus/eth-refutation/POD.txt).
The proofs are decided by two kernels, and the step from each statement to “ETH is false in that lab’s own model” is proved in Lean here (§5, one kernel). What still stands between them and the sentence “ETH is false” is a premise, listed in the order the claim travels through it, each with where its checking stopped:
The weakest premise is assumed. Our Lean ETH is a transcription of the textbook’s, read, and the model and encoding steps are textbook and in no one’s Lean. So this page decides that both proofs check, proves that each statement refutes ETH in its own lab’s model, and reads, without deciding, that ETH is false in the textbook’s model-free sense.
OpenAI (exact_count_and_sat). For every k ≥ 2 there is one machine of the file’s own design (a standard multitape Turing machine with a three-letter alphabet) and constants C, A, d, such that on every set F of clauses of width at most k over n variables, written in the file’s canonical unary encoding of length L, it halts after T ≤ C·(L+1)^d·2^{A·n(ln ln(n+16))²/√ln(n+16)} steps with the exact number of satisfying assignments on one tape and the answer “satisfiable” as its halting state, in polynomial space. Because clauses are sets, L is polynomial in n, so for k = 3 the time is 2^{o(n)}. It does not appear: OAI-C defines no ETH, no s₃ and no reduction. Our bridge supplies it (§5). The exponent is the paper’s Proposition 6.4, weaker by a factor log log n than its headline Theorem 1.1, as OpenAI’s scope note says.
Anthropic (ETHIsFalse, MainTheorem). ETH is 0 < s₃, where s₃ is the infimum of the δ for which some finite machine of Mathlib’s FinTM2 kind and some c ∈ ℕ decide every duplicate-free 3-CNF list within ⌊c·2^{δn}⌋ steps, for every n and any number of clauses. ETHIsFalse is its negation. The Main Theorem gives one machine and one constant C counting the satisfying assignments within ⌊2^{C·min(km/√lg m, k²n lg lg n/√lg n)}⌋ steps, for k ≥ 1, m ≥ 2, n ≥ 4 with every variable occurring.
Both readers, separately: each statement, if proved, implies the textbook ETH (Impagliazzo–Paturi) is false, under the two textbook steps of §2 and nothing else. Neither found a loophole: no padding (the input length is polynomial in n in both), no hidden power in either machine (finite control, finite alphabets, one bounded step at a time), exact halting times, and promises that only restrict where a bound is claimed.
| OpenAI | Anthropic | |
|---|---|---|
| Lean bound | C(L+1)^d·2^{A·n(ln ln(n+16))²/√ln(n+16)}, constants per k | ⌊2^{C·min(km/√lg m, k²n lg lg n/√lg n)}⌋, one absolute C |
| Lean bound against the paper’s | weaker: Proposition 6.4, not Theorem 1.1 | the same, with ranges |
| ETH in Lean | absent from OpenAI’s files (ours: §5) | defined, and its negation proved |
| Machine in Lean | its own multitape machine on Mathlib’s tapes | Mathlib’s FinTM2 (multi-stack) |
| Input in Lean | a set of sets of literals, canonical sorted unary word | a duplicate-free list, fixed-width binary slots |
| Uniform in k | no: for each k a machine | yes: one machine for every k |
| Space | proved polynomial | not stated |
| nanoda in the shipped config | off | on |
Both papers reach the same shapes, n log log n/√log n for any formula and n/√log n for linearly many clauses, and both get their sharpest bound by recursively contracting Boolean tensor networks (OpenAI’s Appendix D, Anthropic’s §2). The two Lean developments formalize different routes: OpenAI’s the interpolation route of its §6.4, Anthropic’s the eight-square recursion.
One computed check. Anthropic’s key identity, eq. (12), the eight-square identity of Degen (1818) and Graves (1843), re-run at this build from the printed formula in exact integer arithmetic: it holds at all 4,096 settings (0 failures). The control, the same formula with i < j in place of i ≤ j, fails at 256, so the check can fail. This decides one printed line of the paper. It decides nothing about the proof.
The textbook definition is written once, in Generic.lean (sha256 78554f883f6c…, byte-identical in both projects). A model fixes four things: what a machine is, which formulas are k-SAT instances, the input word a formula is written as, and what “halts within t steps with answer b” means. Then s_k, the infimum of the δ for which k-SAT is decided within ⌊c·2^{δn}⌋ steps for every n, and ETH, s_k > 0 for every k ≥ 3, read the same in every model. Each lab’s statement is then proved to refute ETH in that lab’s own model:
OpenAI. If OpenAI's challenge statement exact_count_and_sat holds, then ETH (s_k > 0 for every k ≥ 3) is false for PrimitiveMachines on encodeCNF; indeed s_k = 0 for every k ≥ 2 (s_eq_zero_of_claim). The three steps both readers did by hand are Lean lemmas now: the input word is polynomial in n, bitLength_succ_le {n k : ℕ} (F : SAT.CNF (Fin n)) (hF : SAT.WidthAtMost k F) : Encoding.
Anthropic. Anthropic's ETHIsFalse implies that ETH (s_k > 0 for every k ≥ 3) is false for FinTM2 machines on encClauses; the generic DecidesKSat, InTime and s ARE Anthropic's, by definition (decidesKSat_iff, inTime_iff, s_eq). In Lean: s_eq (k : ℕ) : ETHBridge.s model k = MainResults.s k.
How the statements were copied. OpenAI’s challenge file is carried with one declared change: its open theorem exact_count_and_sat becomes the proposition OpenAIClaim, and undoing that change gives back the pinned sha256 4183b2057cff…. Anthropic’s MainResults.lean is carried unchanged (47f78a9550d9…). §1 decided that OpenAI’s proof proves exactly that statement, so the two together give ¬ETH in OpenAI’s model. The join is the identity of the statement’s bytes, not one Lean term: the bridge does not import OpenAI’s proof.
Checked by one kernel. Lean’s, inside lake build on GitHub’s runners (run 40772430556); no sorry, no axiom declared, no native_decide (certs/eth-bridge.json, the README). No second kernel has replayed the bridge.
Not proved, and said so:
The step between the two models, joined by someone else, and replayed here: CERTIFIED. TSavo/eth-bridge @ 34f9ca20 (TSavo; written with Claude, per its README) proves Bridge.
Its gaps, first: