One ocean, or many?
A preprint claims that on every nonamenable symmetric graph there is a window of p with infinitely many infinite clusters: pc < pu
Covers result 214 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:11. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Open each edge with probability p. On the square grid, once p passes the critical value, there is exactly one infinite cluster. On a tree it is different: in our picture of the 3-regular tree at p = 0.75, five big clusters reach the rim, and they can never merge, because a tree has no shortcuts. On the infinite tree, every p between one half and one gives infinitely many infinite clusters at once. So there are two thresholds: pc, where infinite clusters appear, and pu, where they finally merge into one.
On the grid and every graph like it, Burton and Keane’s argument shows the two coincide; those graphs are amenable. In 1996 Benjamini and Schramm conjectured the converse: on every nonamenable symmetric graph, pc is strictly less than pu. Partial results needed extra structure, such as planarity, hyperbolicity, large girth, or a chosen set of generators.
Result 214 is one OpenAI preprint (53 pages, September 24, 2026). It claims the bond form of the conjecture: on every infinite, connected, locally finite, nonamenable quasi-transitive graph, pc < pu, with an interval of p where infinitely many infinite clusters exist at once; in particular every Cayley graph of every finitely generated nonamenable group, for any finite generating set. It goes through a stronger statement Hutchcroft conjectured: at pc, the connection matrix is a bounded operator. A corollary gives the triangle condition and mean-field behaviour; the paper says those power laws come from earlier conditional theorems.
What it doesn’t claim
Site percolation; that pu is below one; any numerical value. We found no earlier claim of the full conjecture, and the paper credits none.
Where it stands
- Posted as a preprint
- OpenAI, 53 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- The general theorem and the Cayley corollary (docs)
Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. Both the general theorem, with its critical laws, and the Cayley corollary are formalized in Lean with the statements pinned down (the general statement): about 154,000 lines in all, 68,000 of them the previous episode’s theorem, imported whole, with no unproved steps; we did not build it. The paper is not among those OSVerify reviewed, and we found no expert reaction.
How the proof goes
- Bounded, though every row is infinite. On the 3-regular tree at pc, each row of the connection matrix sums to infinity, yet the matrix, as an operator, has norm about 8.74 (our exact computation). The paper proves this happens on every graph in the class. Bounded at pc means bounded a little above, and a bounded connection matrix cannot coexist with a single infinite cluster.
- Two cases. Graphs whose automorphism group is not unimodular were done by Hutchcroft and are cited. For the rest, the paper shows critical clusters are rarely huge, by splicing pieces of independent percolation fields.
- Corridors. If the operator were unbounded, cut connections along random corridors. Nonamenability makes random walks escape, so the operator norm barely moves while the row sums drop fast. The two cannot both hold.
Finite simulations can’t see any of this: on a tree times a line, and on the plain grid, one big cluster takes over in the same way.
The numbers in the video
- 3-regular tree (ours, exact): pc = 1/2, p2→2 = 0.707, pu = 1; operator norm at pc 8.74 (finite balls 4.48 up to 6.39 and climbing); Benjamini and Schramm’s 1996 spectral test works on trees only from degree 6 up.
- Simulation (ours): big clusters reaching the boundary at p = 0.7: 3.6 on a tree ball, 1 on a tree times a path, 1 on a grid box. The Lean line counts are ours.
Read the source
- Nonuniqueness of percolation on nonamenable quasi-transitive graphs (PDF), 53 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 214.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Open each edge with probability p. On the square grid, once p passes the critical value, there is exactly one infinite cluster: a single ocean, never several. On a tree, it is different. Here is a tree of degree three at p equal to 0.75: five big clusters reach the rim, and they can never merge, because a tree has no shortcuts. On the infinite tree, every p between one half and one gives infinitely many infinite clusters at once. So there are two thresholds: p_c, where infinite clusters appear, and p_u, where they finally merge into one. Which graphs have a window between them? On the grid and every graph like it, Burton and Keane’s argument shows the two coincide. Those graphs are amenable: some big regions have relatively small boundaries. In 1996, Benjamini and Schramm conjectured the converse: on every symmetric graph whose regions all have large boundaries, a nonamenable graph, p_c is strictly less than p_u. Partial results needed extra structure, such as planarity, hyperbolicity, large girth, or a chosen set of generators. Their own 1996 spectral test, on trees, only works from degree six up, by our computation.
1:16The claim
Result 214 is one OpenAI preprint, 53 pages, dated September 24, 2026, the same day as the previous episode’s. It claims the bond form of the conjecture: on every infinite, connected, locally finite, nonamenable quasi-transitive graph, p_c is less than p_u, with a whole interval of p where infinitely many infinite clusters exist at once. In particular, every Cayley graph of every finitely generated nonamenable group, for any finite generating set. It goes through a stronger statement Hutchcroft conjectured: at p_c, the connection matrix is a bounded operator. A corollary gives the triangle condition at p_c and mean-field critical behaviour; the paper says those power laws come from earlier conditional theorems, and the new input is the bound. Not claimed: site percolation, that p_u is below one, or any numerical value. We found no earlier claim of the full conjecture, and the paper credits none.
2:20How the proof goes
Here is the key phenomenon, on the tree, where our computer can do it exactly. At p_c, each row of the connection matrix sums to infinity, yet the matrix, as an operator, has norm about 8.74. The paper proves that this happens on every graph in the class. Once the operator is bounded at p_c, it stays bounded a little above p_c, and a bounded connection matrix cannot coexist with a single infinite cluster. So there must be many. The graphs whose automorphism group is not unimodular were already done by Hutchcroft, and are cited. For the rest, the paper first shows that critical clusters are rarely huge, by splicing pieces of independent percolation fields. Then it argues by contradiction: if the operator were unbounded, cut connections along random corridors. Nonamenability makes random walks escape, so the operator norm barely moves, while the row sums drop fast. The two cannot both hold. Finite simulations can’t see any of this: on a tree times a line, and on the plain grid, one big cluster takes over in the same way.
3:28Where it stands
The preprint is unrefereed and has not been revised. Both the general theorem, with its critical laws, and the Cayley graph corollary are formalized in Lean, with the statements pinned down: about 154,000 lines in all, 68,000 of them the previous episode’s theorem, imported whole. There are no unproved steps; we did not build it. The paper is not among those OSVerify reviewed, and we found no expert reaction. If it holds, percolation tells amenable graphs from nonamenable ones: on a symmetric graph, for bond percolation, there is a window of many infinite clusters exactly when the graph is nonamenable.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.