Absence of critical Bernoulli bond percolation on $\mathbb Z^d$ in every dimension $d \ge 2$

What the AI did

The repository's own provenance section: the Lean sources, "definitions, statements and proofs, together with Challenge.lean, Solution.lean and the metadata", "were written by an AI system (Anthropic's Claude models) working autonomously under the direction of Justin Leder; no human wrote or edited the Lean code." Its formalization.yaml records the split: "Discovery, informal proof and Lean formalization were all produced by the AI system operating autonomously. Human role (Justin Leder): problem selection, direction, reading of the statement file and metadata, and responsibility for this submission", the author having "posed the problem, set the acceptance standard (kernel-checked proof with the standard axioms, plus adversarial review of the statements) and directed priorities." The same file states that the only review so far was by AI systems, adversarial reads of the formal statements and of the proof chain against the cited literature, and the README asks readers to satisfy themselves that Challenge.lean states the intended theorem rather than relying on the kernel for that - which is the audit recorded under verification here.

Verification

Formalised in Lean 4 in anthropics/formal-math at commit 795efb8. Audited here on 8 September 2026 at four levels. Statement: Challenge.lean read against Grimmett §§1.3-1.4 - the lattice is SimpleGraph.hasse on Fin d → ℤ, whose symmetrised covering relation is nearest-neighbour adjacency; the measure is ProbabilityTheory.setBernoulli on the edge set, whose Mathlib definition was read at source and does mean each edge open independently with probability p; theta is the measure of {|C(0)| = ∞}; p_c is inf {p | theta p > 0} with the empty-case convention declared. Structure: percolation_continuity takes only a dimension and 2 ≤ d, the transport is Iff.rfl, and comparator.json compares exactly the two theorem names permitting only propext, Quot.sound and Classical.choice - so no unproven input can enter as a theorem argument. Counts taken independently across all 251 files and 97,574 lines: no sorry outside the two deliberate placeholders, zero axiom declarations, zero native_decide, zero unsafe. Percolation/Literature/ formalises the classical toolkit rather than assuming it. Not rebuilt here: their run needed a 128-core node and Mathlib from source, so kernel acceptance rests on their audit record, which matched every count I checked. No mathematician has read the argument. Gil Kalai reported it on 3 September with explicit caveats, writing "if verified, this is a remarkable breakthrough" and "we still need to verify if the formalisation is done correctly".

Sources

• Papersummary.pdf: the repository's own guide to the proof
• Lean proofanthropics/formal-math, percolation (Lean 4 development, pinned commit 795efb8) · AUDIT.md: their build, axiom and comparator record
• Lean statementChallenge.lean: the trusted statement, in plain Mathlib
• DiscussionGil Kalai's report, with his caveats
• Otherformalization.yaml: provenance, cost and disclosed divergences