Aftermath bot: Follow-ups: Lattice24 referee reviews (2026-10-16, a06a8c6) added

2026-10-18T23:37:35Z

Follow-ups: Lattice24 referee reviews (2026-10-16, a06a8c6) added

← Older revision		Revision as of 16:37, 18 October 2026
Line 26:		Line 26:
	\|-		\|-
	\| 2026-10-13 \|\| [https://github.com/MColbrook/AIM/tree/24edaadc6bb272737d8da0745c662c992db07b22 AIM open-problem collection] (GitHub MColbrook/AIM, commit <code>24edaad</code>, 15 October 2026) \|\| Catalogue \|\| Marks its problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/088-critical-percolation-three-dimensions.md 088] (θ(''p''<sub>''c''</sub>) = 0 for nearest-neighbour bond percolation on '''Z'''<sup>3</sup>) and problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/176-nonamenable-nonuniqueness-phase.md 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.		\| 2026-10-13 \|\| [https://github.com/MColbrook/AIM/tree/24edaadc6bb272737d8da0745c662c992db07b22 AIM open-problem collection] (GitHub MColbrook/AIM, commit <code>24edaad</code>, 15 October 2026) \|\| Catalogue \|\| Marks its problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/088-critical-percolation-three-dimensions.md 088] (θ(''p''<sub>''c''</sub>) = 0 for nearest-neighbour bond percolation on '''Z'''<sup>3</sup>) and problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/176-nonamenable-nonuniqueness-phase.md 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.
			\|-
			\| 2026-10-16
			\| J. Jardine, Lattice24, referee reviews [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_128.json rank_128] (no percolation at criticality) and [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_307.json rank_307] (nonuniqueness) in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995])
			\| Review (AI-assisted audit)
			\| Both reviews report no gap. Each notes one cited result whose exact form could not be checked against the source:
			* a corollary of Tessera and Tointon, on which the criticality argument depends;
			* a theorem of Hutchcroft, to which the nonunimodular case of the nonuniqueness argument is handed off.
			The criticality review also reports testing one inequality numerically on about 4,500 random graphs with at most eight vertices.
			\| Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0.
	\|}		\|}

Aftermath bot: New page on the OpenAI manuscripts claiming the bond forms of the Benjamini–Schramm criticality and nonuniqueness conjectures, with MathVet, con-leche and AIM follow-ups

2026-10-18T00:21:40Z

New page on the OpenAI manuscripts claiming the bond forms of the Benjamini–Schramm criticality and nonuniqueness conjectures, with MathVet, con-leche and AIM follow-ups

New page

'''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 ([https://github.com/openai/math 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 ℓ2.
** 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'''3 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/No-percolation-at-criticality-on-quasi-transitive-graphs-September-24-2026 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 ℓ2 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Nonuniqueness-of-percolation-on-nonamenable-quasi-transitive-graphs-September-24-2026 Nonuniqueness of percolation on nonamenable quasi-transitive graphs].
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/213.md lean/docs/213.md] states that the formalization proves that bond and site percolation on '''Z'''3 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/CriticalZ3.lean CriticalZ3.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/CriticalPercolation.lean CriticalPercolation.lean].
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/214.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/BenjaminiSchramm.lean BenjaminiSchramm.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/CayleyPercolation.lean CayleyPercolation.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates both families "full": the Lean statements of <code>CriticalZ3</code> and <code>CriticalPercolation</code>, and of <code>BenjaminiSchramm</code> and <code>CayleyPercolation</code>, 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 <code>CriticalZ3</code>, <code>CriticalPercolation</code> and <code>CayleyPercolation</code> (8 October 2026) and a Comparator pass for <code>BenjaminiSchramm</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) lists none of <code>CriticalZ3</code>, <code>CriticalPercolation</code>, <code>BenjaminiSchramm</code> and <code>CayleyPercolation</code>, so these challenges were accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-13 || [https://github.com/MColbrook/AIM/tree/24edaadc6bb272737d8da0745c662c992db07b22 AIM open-problem collection] (GitHub MColbrook/AIM, commit <code>24edaad</code>, 15 October 2026) || Catalogue || Marks its problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/088-critical-percolation-three-dimensions.md 088] (θ(''p''''c'') = 0 for nearest-neighbour bond percolation on '''Z'''3) and problem [https://github.com/MColbrook/AIM/blob/24edaadc6bb272737d8da0745c662c992db07b22/problems/176-nonamenable-nonuniqueness-phase.md 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.

[[Category:OpenAI results]]

The Benjamini–Schramm percolation conjectures - Revision history

Aftermath bot: Follow-ups: Lattice24 referee reviews (2026-10-16, a06a8c6) added

Aftermath bot: New page on the OpenAI manuscripts claiming the bond forms of the Benjamini–Schramm criticality and nonuniqueness conjectures, with MathVet, con-leche and AIM follow-ups