Does it percolate?
Two preprints claim no infinite cluster at the critical point: on the cubic lattice, and on every symmetric graph with pc below one
Covers result 213 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
4:42. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Keep each edge of a grid open with probability p, independently. Small p gives small islands; large p gives one infinite cluster. In between is a critical value pc where an infinite cluster first appears. The question is what happens exactly at pc: is there already an infinite cluster, so that the transition jumps like a cliff, or does it start from zero, like a ramp?
On a tree everything is exact, and it is a ramp. On the square grid, Harris and Kesten settled it, using a symmetry that makes a crossing exactly fifty-fifty at one half. In high dimensions, the lace expansion settled it. But from three dimensions up to ten, above all the cube lattice, it stayed open for decades. In 1996, Benjamini and Schramm conjectured more: no infinite cluster at pc on every symmetric graph, as long as pc is below one.
Result 213 bundles two OpenAI preprints dated September 24, 2026. The first (20 pages) claims no infinite cluster at pc on the cubic lattice, for both bond and site percolation. The second (42 pages) claims the bond form of the Benjamini–Schramm conjecture: on every infinite, connected, locally finite, quasi-transitive graph with pc below one, there is almost surely no infinite cluster at pc. That includes bond percolation on the integer lattice in every dimension from two up.
They were not first on the cube. In August 2026, Justin Leder of Anthropic posted an AI-generated, Lean-checked proof of the bond case on the integer lattice from dimension two up, and work prompted by Ahmed Bou-Rabee (updated September 5) claimed the site case from dimension three. Both OpenAI papers credit them. The new claim here is the general theorem.
What it doesn’t claim
Site percolation on general graphs; any value of pc; critical exponents; rates.
Where it stands
- Posted as preprints
- OpenAI, two papers (20 and 42 pages), dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Both statements (docs)
Last checked October 19, 2026. Neither preprint has been revised since they were added to the repository in its initial commit on October 6, 2026. Both theorems are formalized in Lean with the statements pinned down exactly (the general statement): 10,358 lines for the cube and 68,224 for the general theorem, with no unproved steps; we did not build them. The general Lean proof does not assume the theorems the paper cites, so it must prove them, or substitutes, itself. Neither paper is among those OSVerify reviewed, and we found no expert reaction to them.
How the proof goes
- A finite inequality. If every relay point reaches a target with high probability, then reaching some relay means you probably reach the target. It is a stronger form of an inequality conjectured by Kozma and Nitzan in 2024.
- The cube. If an infinite cluster existed at pc, a finite pattern would show it, and finite patterns survive a tiny decrease in p. A thirteen-move relay carries the connection from cube to cube, and a contour count shows it goes on forever: percolation below pc, which is impossible.
- Every symmetric graph. Sort graphs by how fast their balls grow. Exponential growth was done by Hutchcroft in 2016 and is cited. Faster than any polynomial but slower than exponential: two large clusters would be forced side by side too often. Polynomial growth: the graph hides grid-like coordinates, and a relay along corridors builds an infinite cluster below pc.
The numbers in the video
- Our checks: the gluing inequality held on 2,000 random small graphs, every configuration (no violations, sometimes exact equality; with max in place of min it fails 60 times in 200). Exact crossings on small square blocks are exactly 1/2 at p = 1/2.
- Our simulation on the cubic lattice near pc ≈ 0.2488 (an outside estimate): the chance of reaching distance 24 is still about 0.22 and falling slowly. A finite box cannot tell zero from tiny. The Lean line counts are ours.
Read the source
- Critical bond and site percolation on the cubic lattice (PDF), 20 pages.
- No percolation at criticality on quasi-transitive graphs (PDF), 42 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 213.
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00The question
Keep each edge of a grid open with probability p, independently. Small p gives small islands; large p gives one infinite cluster. In between there is a critical value, p_c, where an infinite cluster first appears. Here is the same random grid at p equal to 0.45, 0.5 and 0.55: scattered clusters, then large ones, then one that takes almost everything. The question is what happens exactly at p_c. Is there already an infinite cluster, so that the transition jumps like a cliff? Or does it start from zero, like a ramp? On a tree of degree three, everything is exact: p_c is one half, and the chance of an infinite cluster rises continuously from zero, at first in a straight line. A ramp. On the square grid, Harris and Kesten settled it, using a symmetry that makes a crossing exactly fifty-fifty at one half; our computer confirms that on small blocks. In high dimensions, the lace expansion settled it. But from three dimensions up to ten, above all the cube lattice, it stayed open for decades. In 1996, Benjamini and Schramm conjectured more: no infinite cluster at p_c on every symmetric graph, as long as p_c is below one.
1:19The claim
Result 213 bundles two OpenAI preprints, both dated September 24, 2026. The first, 20 pages, claims no infinite cluster at p_c on the cubic lattice, for both bond and site percolation. The second, 42 pages, claims the bond form of the Benjamini–Schramm conjecture: on every infinite, connected, locally finite, quasi-transitive graph with p_c below one, there is almost surely no infinite cluster at p_c. That includes bond percolation on the integer lattice in every dimension from two up. They were not first on the cube. In August, Justin Leder of Anthropic posted an AI-generated, Lean-checked proof of the bond case on the integer lattice from dimension two up, and in early September, work prompted by Ahmed Bou-Rabee claimed the site case from dimension three. Both OpenAI papers credit them. The new claim here is the general theorem. Not claimed: site percolation on general graphs, any value of p_c, critical exponents, or rates.
2:27How the proof goes
Both proofs use one finite inequality, a stronger form of one conjectured by Kozma and Nitzan in 2024: if every relay point reaches a target with high probability, then reaching some relay means you probably reach the target. Our computer checked it on 2,000 random small graphs by brute force: no violations, and sometimes exact equality. With max in place of min, it fails 60 times in 200. The cube proof argues by contradiction. If an infinite cluster existed at p_c, a finite pattern would show it, and finite patterns survive a tiny decrease in p. A 13-move relay then carries the connection from cube to cube, and a contour count shows it goes on forever. That is percolation below p_c: impossible. The general paper sorts graphs by how fast their balls grow. Exponential growth was already done by Hutchcroft, in 2016, and is cited. Faster than any polynomial but slower than exponential: two large clusters would be forced side by side too often, and that is too unlikely. Polynomial growth: the graph hides grid-like coordinates, and a relay along corridors builds an infinite cluster below p_c. Our simulation on the cubic lattice shows why proof was needed: near p_c, the chance of reaching distance 24 is still about 0.22 and falling slowly. A finite box cannot tell zero from tiny.
3:56Where it stands
Both preprints are unrefereed and have not been revised. Both theorems are formalized in Lean, with the statements pinned down exactly: about 10,000 lines for the cube and 68,000 for the general theorem, with no unproved steps; we did not build them. The general Lean proof does not assume the theorems the paper cites, so it must prove them, or substitutes, itself. Neither paper is among those OSVerify reviewed, and we found no expert reaction to them. If they hold, critical percolation dies on every symmetric graph with p_c below one, when its edges are random, and the cubic lattice now has three separate claims of the same answer.
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.