The Percolation Claim Compiles. The Question Remains.

Imagine a vast grid of pipes that each open or close at random. Below a tipping point, liquid stays in finite pockets. Above it, endless connected paths become possible. The famous question is what happens exactly at that tipping point: is there already an infinite cluster, or not? For ordinary flat grids and for very high-dimensional ones, mathematicians already knew the answer was no. For the awkward middle dimensions — three through ten — the question stayed open for decades.

In late August 2026 a Claude-written Lean development appeared inside Anthropic’s public formal-math repository claiming to close that gap. It proves a 2024 conjecture by Gady Kozma and Shahaf Nitzan that would imply the result in every dimension at once. There was no launch post and no model card. Most mathematicians first heard about it from Gil Kalai’s blog on 3 September, who called it a claim, not yet a result. Scientific American later framed the episode as an AI solving a holy-grail problem from probability theory. The narrower reading is stranger, and more useful.

A proof assistant can confirm that every step follows from the definitions written in the file. It cannot confirm that those definitions express the theorem a mathematician had in mind. The project’s own README is candid about that seam. It says the work has not been refereed by anyone independent of the author, that correctness rests on the mechanical checks it records, and that readers should verify for themselves that Challenge.lean states the intended theorem. Kalai put the remaining work in the same place on 6 September: check whether the formalisation is done correctly, and wait for experts to digest the argument.

The dying-percolation claim targets θ(p_c) = 0 for nearest-neighbour Bernoulli bond percolation on the integer lattice in every dimension at least two. Continuity of θ on the whole interval is treated as a classical consequence, not as the formal target. The artifact at commit 795efb86 (28 August 2026) includes a README, an audit record, the statement file, and a fifteen-page guide that the README itself calls an aid to reading rather than the warrant. Registry notes credit Justin Leder with directing the work and state that no human wrote or edited the Lean code. An independent structural audit summarised on whataifound reported that the lattice, the Bernoulli measure, θ and p_c matched the intended textbook meanings, with no sorry outside deliberate placeholders — and that no mathematician had yet read the full argument.

As checked on 3 October 2026, the main branch of anthropics/formal-math no longer lists a percolation directory; only the separate zeta23 formalisation remains visible there. The percolation files still exist at the pinned commit. That does not prove the claim was withdrawn or wrong. It does mean the artifact is no longer where a casual link to main expects it.

The interesting find is not another headline that an AI proved a theorem. It is the seam that remains after the machine finishes: between a compiling formal statement and a result the field can treat as settled.