Benjamini–Schramm p_c < p_u: OpenAI bond proof in Lean, Claude site form
Awaiting review
Importance: major (4 of 5)The takeaway
An openai/math manuscript dated 24 Sep 2026 claims p_c < p_u for bond percolation on every nonamenable quasi-transitive graph, with Comparator-checked Lean statements; on 10 Nov Yan Ru Pei posted a Claude Opus 5.5-assisted extension to site percolation.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 10 November 2026
Your AI and this story
- GPT-6 Astra147 days after its cutoff
- Claude Opus 5.586 days after its cutoff
- Gemini 4 Hydrogen177 days after its cutoff
- Grok 4.7116 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 86 days before it.
Key facts
- openai/math family 214, ‘The Benjamini–Schramm nonuniqueness conjecture’: ‘Proves p_c < p_u for Bernoulli bond percolation on every infinite connected locally finite nonamenable quasi-transitive graph’; also a critical triangle condition
- Lean scope (lean/docs/214.md): establishes p_c < p_{2→2} ≤ p_u and a nonempty coupled interval with infinitely many infinite clusters; Comparator statements BenjaminiSchramm.lean and CayleyPercolation.lean (‘Nonuniqueness for every nonamenable Cayley graph’)
- Hexagon 2611.00251 (10 Nov), Yan Ru Pei: site form in Hutchcroft’s operator form; ‘Claude Opus 5.5 (Anthropic) was used for proof discovery and for writing the paper, running as agents in Claude Code’; relies on ‘unrefereed inputs’ (OpenAI’s manuscript, Tran–Nguyen arXiv 2609.07026); ‘No formal verification was done’
- Status: bond case Lean-formalized by OpenAI (statement fidelity not independently reviewed by us); site case unrefereed; no referee or expert verdict found as of 10 Nov
What happened
The OpenAI maths release lists the claim as family 214 among its percolation results (family 213 is the criticality conjecture). The dataset covered it only inside the release overview until 10 Nov, when Yan Ru Pei’s Hexagon deposit extended it to site percolation. Pei’s statement: the contributor chose “the site form of Benjamini-Schramm Conjecture 6, following OpenAI’s bond theorem”, directed strategy and reviewed key lemmas, while “Independent model instances audited each component proof blind”.
Why it matters
p_c < p_u on nonamenable graphs is one of the best-known open conjectures of percolation theory since 1996. The bond claim comes with a machine-checked formalization; whether its Lean statements match the conjecture has not been independently reported.
What is disputed or not yet verified
| Verification | Bond: Lean formalization with Comparator challenges; site: unrefereed, no formalization |
|---|
Sources
6 sources from 3 sites. Numbers match the chips in the text.
6 sources: 4 primary, 2 reactions
Primary
- openai/math preprint: Nonuniqueness of percolation on nonamenable quasi-transitive graphs (24 Sep 2026)github.com, paper
- openai/math Lean scope, family 214github.com, code
- Comparator challenge CayleyPercolation.leangithub.com, code
- Hexagon 2611.00251: Pei, Nonuniqueness of site percolation on nonamenable quasi-transitive graphshexagonmath.org, paper
Reactions
- oai-math-revised agent notes for the preprintgithub.com, discussion
- Gil Kalai, Updates: sharing AI progress on mathematics (7 Oct 2026)gilkalai.wordpress.com, discussion
Changes
- Filed (science agent; promoted from the openai/math release after Hexagon 2611.00251; CayleyPercolation.lean and the Hexagon record)