The Benjamini–Schramm percolation conjectures

The Benjamini–Schramm percolation conjectures are two conjectures about Bernoulli percolation on quasi-transitive graphs from Benjamini and Schramm's 1996 paper Percolation beyond Z^d, many questions and a few answers. The first (their Conjecture 4) asserts that there is no infinite cluster at the critical probability p_c whenever p_c < 1. The second (their Conjecture 6) asserts that every nonamenable quasi-transitive graph has a nonempty phase with infinitely many infinite clusters, that is, p_c < p_u. Three manuscripts dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim the bond-percolation forms of both conjectures, and both the bond and the site case of the first on the cubic lattice. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introductions of the manuscripts:
  • For nearest-neighbour percolation on Z^d, planar methods settled critical nonpercolation in dimension two (Harris and Kesten for bond percolation, Russo for site percolation on the square lattice). The lace expansion of Hara and Slade settled it in sufficiently high dimensions, and Fitzner and van der Hofstad obtained the nearest-neighbour bond range d ≥ 11. The cubic lattice remained open.
  • Beyond lattices, Benjamini, Lyons, Peres and Schramm proved critical nonpercolation for nonamenable graphs with a unimodular quasi-transitive action. Timár excluded infinitely many infinite critical clusters on nonunimodular transitive graphs. Hutchcroft excluded infinite critical clusters on every quasi-transitive graph of exponential growth, and Hermon and Hutchcroft treated unimodular graphs satisfying a stretched-exponential return-probability bound.
  • For nonuniqueness, Benjamini and Schramm proved 0 < p_c < p_u < 1 for one-ended nonamenable transitive planar graphs, for both bond and site percolation, following Lalley's work on Fuchsian groups. Schonmann treated a highly nonamenable regime, Nachmias and Peres graphs of large girth, and Gaboriau graphs admitting nonconstant harmonic Dirichlet functions. For Cayley graphs, Pak and Smirnova-Nagnibeda, and later Thom, showed that a suitable generating set gives nonuniqueness.
  • Hutchcroft's operator-threshold conjecture asks for the stronger strict inequality p_c < p_2→2, where p_2→2 is the supremum of the parameters at which the two-point connection kernel is bounded on ℓ².
  • The nonuniqueness manuscript notes that Benjamini and Schramm's standing model is site percolation and that they extend their nonplanar questions to bond percolation.

The original results

• Critical bond and site percolation on the cubic lattice (24 September 2026). Theorem 1.1 of the manuscript states that nearest-neighbour Bernoulli bond percolation on Z³ has almost surely no infinite open cluster at the bond critical parameter, and that the same holds for nearest-neighbour site percolation at the site critical parameter. Source: the manuscript Critical bond and site percolation on the cubic lattice.
• No percolation at criticality on quasi-transitive graphs (24 September 2026). Theorem 1.1 of the manuscript states that critical Bernoulli bond percolation has no infinite cluster on every infinite connected locally finite quasi-transitive graph with p_c < 1; this includes nearest-neighbour bond percolation on Z^d for every d ≥ 2. The abstract describes this as resolving the bond form of the criticality conjecture. The manuscript uses Hutchcroft's theorem for graphs of exponential growth and gives its own arguments for the remaining subexponential case. Source: the manuscript No percolation at criticality on quasi-transitive graphs.
• Nonuniqueness of percolation on nonamenable quasi-transitive graphs (24 September 2026). Theorem 1.1 of the manuscript states that, for Bernoulli bond percolation on every infinite connected locally finite nonamenable quasi-transitive graph, the critical connection kernel is bounded on ℓ² and p_c < p_2→2 ≤ p_u, with a nonempty interval of parameters at which there are almost surely infinitely many infinite clusters simultaneously. A corollary covers every finite symmetric generating set of every nonamenable finitely generated group. A further corollary gives the triangle condition at p_c and mean-field critical behaviour, and states that this verifies two further conjectures of Hutchcroft. The manuscript describes its main theorem as a positive resolution of the bond-percolation nonuniqueness conjecture and of Hutchcroft's operator-threshold conjecture. Source: the manuscript Nonuniqueness of percolation on nonamenable quasi-transitive graphs.
• Formalization, as described by the repository.
  • The scope note lean/docs/213.md states that the formalization proves that bond and site percolation on Z³ have no infinite cluster at their critical probabilities, and that critical bond percolation has no infinite cluster on every infinite connected locally finite quasi-transitive graph with p_c < 1, with bond multiplicities allowed. Its Comparator challenges are CriticalZ3.lean and CriticalPercolation.lean.
  • The scope note lean/docs/214.md states that the formalization proves the nonuniqueness phase conjecture for Bernoulli bond percolation in the same graph class, with p_c < p_2→2 ≤ p_u and a common coupled interval, the Cayley-graph statement for every finite symmetric generating set, and the selected critical estimates. Its Comparator challenges are BenjaminiSchramm.lean and CayleyPercolation.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 18 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates both families "full": the Lean statements of CriticalZ3 and CriticalPercolation, and of BenjaminiSchramm and CayleyPercolation, state the headline claims. It lists the hand-written Følner definition of amenability in the Cayley statement among the definitions to check. Its per-challenge table records sandboxed Comparator passes for CriticalZ3, CriticalPercolation and CayleyPercolation (8 October 2026) and a Comparator pass for BenjaminiSchramm.	The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists none of CriticalZ3, CriticalPercolation, BenjaminiSchramm and CayleyPercolation, so these challenges were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-13	AIM open-problem collection (GitHub MColbrook/AIM, commit 24edaad, 15 October 2026)	Catalogue	Marks its problem 088 (θ(pc) = 0 for nearest-neighbour bond percolation on Z3) and problem 176 (a nonuniqueness phase on every nonamenable transitive graph) as solved by the OpenAI manuscripts, after a dated statement comparison of 13 October 2026.	The records describe this as an AI statement-level review of the published manuscripts, not an independent audit of the proofs or a Lean kernel replay.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.