Lean proof that the percolation probability vanishes at the critical point in every dimension
A Lean development proves that nearest-neighbour Bernoulli bond percolation on the integer lattice has no infinite cluster at its critical parameter in every dimension at least two, which would settle the dimensions 3 to 10 that were open.
- Lab
- Anthropic
- Model
- Anthropic Claude models, versions not stated
- Field
- Mathematics
- Date
- 2026-08-28
- Human collaborators
- Justin Leder
What was found
The development proves Kozma and Nitzan's Conjecture 3 (arXiv:2401.12397), which by their Theorem 6 gives that the percolation probability vanishes at the critical point on the d-dimensional integer lattice for every d at least 2. The route is a new conditioned slack hierarchy, a family of conditioned covariance inequalities for increasing functions of a single open cluster whose level-zero case is the Harris inequality, from which a stronger additive gluing inequality is derived. The classical inputs, including Harris, van den Berg, Haggstrom and Kahn, the four functions theorem, Gladkov's decision-tree Harris-Kleitman inequality, the Barsky, Grimmett and Newman half-space theorem and Kesten's critical value for the square lattice, are re-proved from Mathlib, so the statement carries no hypothesis beyond the dimension. The recorded audit reports a clean build, two sorry placeholders confined to the statement file by design, no added axioms, all seven compared theorems depending on exactly the three standard axioms, and a passing comparator run.
Novelty check
The result was known for dimension two by Harris and Kesten and for dimension at least eleven by the lace expansion of Hara and Slade and of Fitzner and van der Hofstad; the repository cites Grimmett's Percolation and Duminil-Copin's 2018 ICM conjecture for the standing of the open cases 3 to 10. The proved statement is Kozma and Nitzan's Conjecture 3, posed in 2024 and open at the time of writing. The repository is explicit about what is not claimed: their Conjectures 1, 2 and 4, anything about slabs, site percolation or other lattices, and continuity of the percolation probability as a formal statement. No competing claim on Conjecture 3 was found in the four registries or on arXiv.
Caveats and known objections
The artifact is not published where it says it is, and that is the first thing to check before citing it. The percolation directory does not exist on the main branch of anthropics/formal-math, whose project table lists only the zeta23 formalization; no branch carries it and the repository's own commit history for that path is empty. It survives only at the pinned commit recorded in the sources here, and the README's own repository link and AUDIT.md both point at a main-branch path that now returns 404. Verification is graded claimed rather than formal despite a passing comparator run, for two reasons: no human has read it, and the statement fidelity question is load-bearing here in a way it is not for a formalization of a known theorem. The README says so itself, that the work 'has not yet been refereed by human mathematicians or by anyone independent of the author; the only review so far was carried out by AI systems', and that readers should check that Challenge.lean states the intended theorem. There is no registration at Palomar. Autonomy is ai-led on the repository's own wording, that the Lean was written by an AI system 'working autonomously under the direction of Justin Leder; no human wrote or edited the Lean code': the direction is human, so the strictest defensible reading is not autonomous.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Lean proof that the percolation probability vanishes at the critical point in every dimension. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-28-percolation-critical-pointBibTeX
@misc{whataifound-anthropic-2026-point,
title = {Lean proof that the percolation probability vanishes at the critical point in every dimension},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Anthropic. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-08-28-percolation-critical-point}
}