Two AI proofs of critical percolation, checked against the textbook statement I wrote

• In the single-Lean check, OpenAI’s proof is a port. To put both proofs in one Lean (section 4), OpenAI’s ℤ³ proof was moved to the version Anthropic’s uses: 22 of its 34 files changed, almost all of them renamed library lemmas. Its statement file is unchanged, byte for byte, and the moved proof is accepted against it. It is still not OpenAI’s proof as shipped; that one was checked on its own version.
• Not the papers. This checks the Lean statements against the textbook’s definitions. It does not check either lab’s informal argument, or Kozma and Nitzan’s reduction as printed.
• Anthropic’s proof is not on its repository’s main branch. It is reachable only by its commit hash (the pull request was closed the same day); I pinned that commit by its hash.
• The same model family. The bridge to Anthropic’s proof was written by Claude, Anthropic’s model. The kernels decide, not the model; you should still know.
• Lean and Mathlib are trusted, as in any check of this kind.

From Grimmett’s Percolation (2nd ed., 1999, §1.3–1.4): ℤ^d with an edge between points at distance one; each edge open with probability p, independently; θ(p) the probability that the origin’s open cluster is infinite; p_c the supremum of the p with θ(p) = 0. The claim: θ(p_c) = 0 in every dimension d ≥ 2. I wrote it in Lean after reading the two labs’ statement files and none of their proofs, and encoded it differently from both on purpose, so that a bridge has to show the encodings agree.

def Adjacent (x y : Vertex d) : Prop := ∑ i, |x i - y i| = 1
def Edge (d) := {e : Sym2 (Vertex d) // Sym2.lift ⟨Adjacent, _⟩ e}
def P (d) (p) := Measure.infinitePi fun _ : Edge d => bernoulliMeasure true false p
def θ (d) (p) := (P d p {ω | (cluster ω 0).Infinite}).toReal
def pc (d) := sSup {p : ℝ | ∃ h : p ∈ Set.Icc 0 1, θ d ⟨p, h⟩ = 0}
def Statement := ∀ d, 2 ≤ d → ∃ h : pc d ∈ Set.Icc 0 1, θ d ⟨pc d, h⟩ = 0

Abridged; the full file is 71 lines, in the record.

• It cannot be satisfied trivially. Proved in my encoding, at both Lean versions and inside both labs’ environments: θ(0) = 0, θ(1) = 1, and p_c lies in [0, 1] with no hypothesis, so the supremum is never Lean’s default for an empty set. With them, the statement forces p_c < 1.
• Sealed first. The file’s fingerprint was registered before any of the labs’ code was built here, and the file never changed.

• It replays as shipped. Commit 795efb86 builds in 9 minutes. The 7 theorems its audit names rest on the three standard axioms of Lean only. Its own Comparator check passes with Lean’s kernel and nanoda, and refuses 2 planted wrong statements. Lean’s checker replays the whole environment from scratch in 36 minutes.
• The bridge. A 299-line Lean file proves my statement for every d ≥ 2 from Anthropic’s main theorem. It matches the two graphs, carries my product measure to theirs, identifies the clusters, and turns their p_c (an infimum) into mine (a supremum) with their proof that θ increases with p.
• Checked with my statement as the target. Comparator, given my file as the statement to be proved, accepts on Lean’s kernel and on nanoda. Lean’s checker replays the bridge’s whole environment from scratch in 32 minutes.

• The bridge. A 306-line Lean file proves my statement at d = 3 from the bond part of OpenAI’s ℤ³ theorem (critical_no_infinite, openai/math at 4eaee875).
• One lemma was missing. OpenAI’s ℤ³ library does not state that θ increases with p, which the step from its infimum p_c to the textbook’s supremum needs. The bridge proves it by the standard coupling, in 79 lines. That piece is ours.
• Checked with my statement as the target. Comparator accepts on Lean’s kernel and on nanoda; Lean’s checker replays the whole environment from scratch in 36 minutes.

• Why. The two bridges first ran on two Lean versions: Anthropic’s on v4.32.0, OpenAI’s on v4.34.1. My statement was the same file in both, but of the 2,488 library definitions it reaches, only 2,032 are identical across the two. That it meant the same thing in both was a careful reading. This section replaces the reading with a check.
• The port. OpenAI’s ℤ³ proof was moved to Lean v4.32.0: 22 of 34 files changed (124 lines out, 125 in), 12 untouched. OpenAI’s statement file and all of Anthropic’s library are unchanged; my statement and the bridge to Anthropic’s proof are the sealed files; the bridge to OpenAI’s proof changed in 3 lines.
• What was checked there. One environment now holds both proofs, both bridges and my statement. It builds from empty with no error and no warning. Comparator, given my file as the statement to be proved, accepts both results on Lean’s kernel and on nanoda: every d ≥ 2 from Anthropic’s proof, d = 3 from OpenAI’s. It also accepts the moved proof against OpenAI’s own unchanged statement file. Lean’s checker replays the whole environment from scratch in 33 minutes.
• Planted errors, again. In that environment, 8 builds against a false statement (θ(p_c) = 1, and the false p_c of R4 below) all fail, each inside a bridge.
• The first run failed, by my own packaging. My archive of the inputs carried 34 stray files from macOS into the library, and the build stopped on them. I removed them, compared the tree with its list file by file, and ran every check again from an empty build. Both runs are in the records.

• R1 · θ(p_c) = 1. False. Both bridges fail on it.
• R2 · the statement at d = 1 (A) / p_c of ℤ¹ (O). False. Both bridges fail on it. The d = 1 statement is also proved false in Lean, in a 202-line file that uses Mathlib only, at both Lean versions: in one dimension p_c = 1 and θ(1) = 1, so the condition d ≥ 2 in my statement is needed.
• R3 · p_c as inf {θ > 0}. Still true, as it turned out, so its failure shows only that the bridges depend on how p_c is written. Not counted as a refusal; R4 replaced it.
• R4 · p_c as sup {θ > 0}. False, and proved false in Lean in the same environment. Both bridges fail on it.

• Rules first. The rules for each stage were written and sealed before the stage ran: a salted fingerprint of the private work, posted to a public registry and to Bitcoin, which proves the date without showing the content (6 seals). Each departure from the rules is listed in the records.
• Written by agents, checked by me. Claude agents wrote the two bridges, the port and the d = 1 proof on rented machines. I rebuilt each, listed their axioms and ran both kernels and the full replays myself; the single-Lean check is my own run, from the agent’s saved files.
• Size. One day, 12 November 2026: a laptop and 5 rented machines, about US$5.38.

• The proofs. Anthropic (Justin Leder with Claude) and OpenAI. Both build on Kozma and Nitzan’s reduction.
• The statement. Geoffrey Grimmett’s textbook; written in Lean by me.
• The checkers. Lean, Mathlib, Comparator and nanoda: their authors.
• The bridges and the checks on this page. Carlos Toledo, with Claude (Anthropic), which wrote the programs and the Lean under my direction.

• The record. node tools/record-percolation-critical.js --check re-derives every number on this page from corpus/percolation-critical (588 files, each pinned by its hash) and refuses on any difference.
• The records as written. The rules sealed before each stage, every run’s log, the bridges and the statement, gaps first: corpus/percolation-critical/results/percolation/VERDICT.md.
• What was checked. anthropics/formal-math at 795efb86 and openai/math at 4eaee875.
• The note. The report and the records, deposited: doi:10.5281/zenodo.24175228.