---
id: "2026-09-24-benjamini-schramm-pc-pu-nonamenable-openai-lean"
url: "https://postcutoff.com/e/2026-09-24-benjamini-schramm-pc-pu-nonamenable-openai-lean/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2026-09-24"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 6
editor: human editor
human_review: null
version: "2026-11-10"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-09-24-benjamini-schramm-pc-pu-nonamenable-openai-lean/

# Benjamini–Schramm p_c < p_u: OpenAI bond proof in Lean, Claude site form

Full title: OpenAI's openai/math claims the Benjamini–Schramm p_c < p_u conjecture (1996) for bond percolation, with a Lean formalization; a Claude-agent site version follows on Hexagon

Benjamini and Schramm conjectured in 1996 that Bernoulli percolation on every nonamenable quasi-transitive graph has a phase with infinitely many infinite clusters (p_c < p_u). OpenAI's openai/math release contains a manuscript dated 24 Sep 2026 claiming the bond case, building on Hutchcroft's operator approach, with a Lean formalization and Comparator challenges. On 10 Nov 2026 a Hexagon deposit by Yan Ru Pei, produced with Claude Opus 5.5 agents, claims the site case, which contains the bond case.

## 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 147 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 86 days after its cutoff
- Gemini 4 Hydrogen (training cutoff March 2026): 177 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 116 days after its cutoff

## Sources

1. [openai/math preprint: Nonuniqueness of percolation on nonamenable quasi-transitive graphs (24 Sep 2026)](https://github.com/openai/math/blob/main/preprints/Nonuniqueness-of-percolation-on-nonamenable-quasi-transitive-graphs-September-24-2026/paper.pdf) (github.com, paper)
2. [openai/math Lean scope, family 214](https://github.com/openai/math/blob/main/lean/docs/214.md) (github.com, code)
3. [Comparator challenge CayleyPercolation.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/CayleyPercolation.lean) (github.com, code)
4. [Hexagon 2611.00251: Pei, Nonuniqueness of site percolation on nonamenable quasi-transitive graphs](https://hexagonmath.org/abs/2611.00251) (hexagonmath.org, paper)
5. [oai-math-revised agent notes for the preprint](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/Nonuniqueness-of-percolation-on-nonamenable-quasi-transitive-graphs-September-24-2026/AGENT_NOTES.md) (github.com, discussion)
6. [Gil Kalai, Updates: sharing AI progress on mathematics (7 Oct 2026)](https://gilkalai.wordpress.com/2026/10/07/updates-sharing-ai-progress-on-mathematics-amazing-and-my-lecture-plans/) (gilkalai.wordpress.com, discussion)

## Changes

- 2026-11-10 (filed): Created (science agent; promoted from the openai/math release after Hexagon 2611.00251; CayleyPercolation.lean and the Hexagon record)

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-09-03: [Claude-written Lean proof claims the dying percolation conjecture θ(p_c)=0 in every dimension](https://postcutoff.com/e/2026-09-03-dying-percolation-theta-pc-zero/index.md)