AI Proved What?

Episode 226, October 2026

Two random tilings, one loop soup?

A preprint claims double-dimer loops in the half-plane converge to CLE4 as curves

Covers result 226 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

4:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:11The claim
  3. 2:00How the proof goes
  4. 3:42Where it stands

The claim, in plain words

Cover a grid with dominoes; Kasteleyn’s formula counts them exactly, 12,988,816 tilings of an 8-by-8 board. Draw two independent random tilings on the same board and overlay them: where they agree you see a doubled domino, and everywhere else the dominoes join into closed loops that alternate between the two tilings. This is the double-dimer model, a random soup of nested, non-crossing loops.

A conjecture credited to Kenyon says that, zoomed out, these loops become CLE4, the conformal loop ensemble that traces level lines of the Gaussian free field. Kenyon, Dubédat, Basok and Chelkak, and Bai and Wan proved step by step that the loops’ topology converges, as Basok and Izyurov restated for the half-plane: how each loop winds around marked points, and how they nest. But as recently as January 2025, experts wrote that convergence of the loops themselves, as curves, remained open: the model lacks the crossing estimates that usually give compactness.

Result 226 is one OpenAI preprint, 33 pages, dated September 23, 2026. It claims that missing step in one setting: on the square lattice in the upper half-plane, with the standard Temperleyan boundary, the complete nested loop ensemble converges to nested CLE4, matching every macroscopic loop as an unparametrized curve, along the full mesh limit. Which CLE it is comes from the earlier work; what is new is compactness of the loops as curves, and the step from puncture data to curves.

What it doesn’t claim

Bounded domains, other graphs or boundary conditions, paths between boundary points, or rates of convergence.

Where it stands

Released as a preprint
OpenAI, 33 pages, dated September 23, 2026
Peer reviewed
Not yet
Checked in Lean
Not formalized

Last checked October 19, 2026. The preprint has not changed since it was added to the repository in its initial commit on October 6, 2026, and there is no Lean for it. Not among those OSVerify reviewed; we found no expert reaction and no competing claim. Release item 223 claims CLE4 for a different model, the random-cluster model at q = 4, by an unrelated route; neither cites the other.

How the proof goes

  1. Exact transfer matrices. In a finite rectangle, scan column by column: the horizontal dominoes crossing each seam, with alternate rows flipped, behave like particles, and one column step is a free-fermion transfer matrix whose spectrum, and the exact number of tilings, the paper computes. Moving k particles between the two tilings costs a penalty growing like k², so many loop crossings of a strip are extremely unlikely, with no prior crossing bound assumed.
  2. Short segments. A two-particle insertion on a short segment has tiny but signed entries; a positivity argument, with weights that at least halve down each nesting chain, turns the signed sum into a bound on bad crossings.
  3. Half-plane and identification. Wilson’s algorithm, through Temperley’s bijection with spanning trees, carries both estimates to the half-plane. The crossing bounds give compactness; then puncture data pin each limit loop to a CLE4 loop, ruling out invisible excursions and backtracking.

The numbers in the video

  • Ours: the paper’s exact tiling formula equals direct counts (for example 192 tilings of the 5-by-5 Temperleyan board, the number of spanning trees of a 3-by-3 grid); our sampler is exactly uniform.
  • Ours: 7,550 overlaid pairs on squares up to 800 wide. Nesting around a point grows at 0.097 per e-fold of scale (CLE4: 1/π² ≈ 0.101); loop length grows with diameter to the power 1.47 (3/2 predicted); no sample crossed the middle third more than four times. Finite squares, not the half-plane: illustration only.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The question

Cover a grid with dominoes, each covering two neighboring squares. Kasteleyn’s formula counts them exactly: an 8-by-8 chessboard has 12,988,816 tilings. Now draw two independent random tilings on the same board and lay one over the other. Where they agree you see a doubled domino; everywhere else the dominoes join into closed loops that alternate between the two tilings. This is the double-dimer model: a random soup of nested, non-crossing loops. A conjecture credited to Kenyon says that, zoomed out, these loops become CLE₄, the conformal loop ensemble that also traces level lines of the Gaussian free field. Step by step, Kenyon, Dubédat, Basok and Chelkak, and Bai and Wan proved that the loops’ topology converges, as Basok and Izyurov restated for the half-plane: how each loop winds around marked points, and how they nest. But as recently as January 2025, experts wrote that convergence of the loops themselves, as curves, remained open: the model lacks the crossing estimates that usually give compactness.

1:11The claim

Result 226 is one OpenAI preprint, 33 pages, dated September 23, 2026. It claims that missing step in one setting: on the square lattice in the upper half-plane, with the standard Temperleyan boundary, the complete nested loop ensemble converges to nested CLE₄, matching every macroscopic loop as an unparametrized curve, along the full mesh limit. Which CLE it is comes from the earlier work: the paper imports the topological convergence from Basok and Izyurov’s restatement. What is new is compactness of the loops as curves, and the step from puncture data to curves. Not claimed: bounded domains, other graphs or boundary conditions, paths between boundary points, or rates.

2:00How the proof goes

The new estimates live in a finite rectangle. Scan it column by column: the horizontal dominoes crossing each seam, with alternate rows flipped, behave like particles, and one column step is a free-fermion transfer matrix, whose spectrum the paper computes exactly, along with the exact number of tilings. Moving k particles between the two tilings costs a penalty growing like k², so many loop crossings of a strip are extremely unlikely, with no prior crossing bound assumed. A second estimate inserts a two-particle operator on a short segment. Its entries are tiny but signed, and a positivity argument, with weights that at least halve down each nesting chain, turns the signed sum into a bound on bad crossings. Wilson’s algorithm, through Temperley’s bijection with spanning trees, carries both estimates from rectangles to the half-plane. The crossing bounds give compactness; then puncture data pin each limit loop to a CLE₄ loop, ruling out invisible excursions and backtracking. As an illustration, our computer checked the paper’s exact tiling formula against direct counts, sampled exactly uniform tilings with Wilson’s algorithm, and overlaid 7,550 pairs on squares up to 800 wide. Loops around a point accumulated at 0.097 per e-fold of scale, against CLE₄’s 1/π², about 0.101. Loop length grew with diameter to the power 1.47, against 3/2. And no sample crossed the middle third more than four times, at any size.

3:42Where it stands

The preprint is unrefereed and unchanged since release. There is no Lean for it. It is not among those OSVerify reviewed, and we found no expert reaction and no competing claim. Another release paper, 223, claims CLE₄ for a different model, the random-cluster model at q equal to four, by an unrelated route; neither cites the other. If it holds, double-dimer loops in the half-plane become CLE₄ as curves, not just in their topology, closing, in the half-plane, the gap the experts named; general domains remain open.

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.