VibeMathedMath problems solved with AI
Sign in

Absence of critical Bernoulli site percolation on Zd\mathbb Z^d for d≥3d \ge 3

For nearest-neighbour Bernoulli site percolation on Zd\mathbb Z^d, each vertex is open independently with probability pp. Let θ(p)\theta(p) be the probability that the open cluster of the origin is infinite and pcp_c the critical parameter. Is θ(pc)=0\theta(p_c)=0 for every d≥3d \ge 3? This is the site form of the classical question of no percolation at criticality; Benjamini and Schramm stated it for site percolation on every quasi-transitive graph with pc<1p_c<1. The planar case was settled classically, and high dimensions by Heydenreich and Matzke's site lace expansion (2020), with no explicit dimension bound.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Percolation theory; mathematical statistical mechanics
Posed by
Itai Benjamini and Oded Schramm, Percolation beyond Z^d, many questions and a few answers (1996), Conjecture 4, stated for site percolation
Year posed
1996
Years open
30y
Solved
2026-09-05
Model
ChatGPT 5.6 (per the exposition page; the author's other documents also name Claude and GLM models)
Vendor
OpenAI; Anthropic; Zhipu AI
Collaborators
Ahmed Bou-Rabee, Justin Leder
Verification
Lean-checked, statement unaudited
Publication
Announced
Significance
72 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Claims θ(pc)=0\theta(p_c)=0 for nearest-neighbour Bernoulli site percolation on Zd\mathbb Z^d for every d≥3d\ge3 (theorem KNAll.Site.site_no_percolation_at_critical), by proving the Kozma-Nitzan gluing inequality for independent hyperedges, representing site percolation by incidence hyperedges, and running the lattice exploration of the bond proof. The intermediate dimensions were open. The planar case is classical and outside the formal statement. The same repository proves Kozma-Nitzan Conjectures 1 to 4 and 6, answers Questions 5, 7 and 9, and refutes one reading of Question 8. OpenAI's release (24 September 2026) later gave critical site nonpercolation on Z3\mathbb Z^3 only, crediting this work; its quasi-transitive theorem is bond only, so the site form of Benjamini-Schramm Conjecture 4 beyond Zd\mathbb Z^d stays open.

What the AI did

The public exposition (Bou-Rabee's site, last updated 5 September 2026) says: "Mathematics generated by ChatGPT 5.6, prompted by Ahmed Bou-Rabee, with exposition and formalization support by Claude Opus 5 and GLM 5.3." The companion manuscript on the Kozma-Nitzan inequalities says its arguments, exposition and Lean formalization "were produced entirely by ChatGPT 5.6 Sol and Claude Fable 5.1, prompted by Ahmed Bou-Rabee", and the repository NOTICE says the KN, hypergraph and site development was "produced with ChatGPT and Claude, prompted by Ahmed Bou-Rabee". The repository's formalization.yaml names Bou-Rabee and Justin Leder as authors (Leder as responsible maintainer) and lists Claude Opus 5.5, Sonnet 5, Opus 5 and DeepSeek v4.1 Flash as the Lean agents, closely supervised by Bou-Rabee. The model lists differ between documents; all agree the mathematics came from the models.

Verification

No independent mathematician has checked this yet. Checked here on 7 October 2026 at commit 6a76bc3f of nitromannitol/percolation-after-anthropic: the Mathlib-only comparator challenge PercolationAudit/SiteCriticality/Challenge.lean was read. It builds nearest-neighbour Z^d as SimpleGraph.hasse on Fin d to Z (as in the audited bond entry), the product Bernoulli law on vertex sets, open clusters through open vertices, theta as the law of an infinite cluster at the origin and p_c as the infimum of percolating parameters with 1 adjoined, and states thetaSite d (p_c) = 0 for every d with 3 <= d and no other hypothesis. That is the headline claim. The repository's CI shows the Comparator audit workflow succeeding on that commit; formalization.yaml reports no sorry and only propext, Classical.choice and Quot.sound. Not rebuilt here. The proof depends on Anthropic's bond library pinned at 795efb8, audited for the bond entry. The site extension has no written proof outside the exposition and the Lean development.

Sources

Changelog1 change

Discussion