Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Random-cluster interfaces: critical, disordered, thermal, and natural-time scaling

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves chordal SLEκ limits for critical square-lattice random-cluster interfaces for \(0\lt q\le4\), with \(\kappa=4\pi/\arccos(-\sqrt q/2)\): bounded Jordan domains are allowed for q ≥ 1, and smooth Jordan domains for q < 1, under the stated marked-boundary approximations. For \(1\le q\le4\), complete nested plane loops converge to CLEκ.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1 (Interfaces and all nested loops)

In Square-lattice FK interfaces and nested loops for 1 <= q < 4, 23 September 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

For every fixed real 1\le q<4, the following assertions hold.

  1. (i)

    For every bounded Jordan domain D with distinct boundary marks a,b, and every approximation satisfying (1.3), the Dobrushin strand \eta_n converges in law, in (1.4), to chordal \SLE_{\kappa(q)} from a to b in D.

  2. (ii)

    Under the specified free infinite-volume law, \Gamma_\delta converges in law as \delta\downarrow0 to the nested whole-plane \CLE_{\kappa(q)}, in the spherical collection topology just defined. The limit is Möbius invariant.

Both conclusions hold along every mesh sequence. No uniformity in q is asserted.

Theorem 1.1 (Interfaces and all nested loops)

In Conformal Limits of Critical Square-Lattice Random-Cluster Interfaces, 5 October 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

For every fixed real 1\le q\le4, the following assertions hold.

  1. (i)

    For every bounded Jordan domain D with distinct boundary marks a,b, and every approximation satisfying (1.3), the Dobrushin strand \eta_n converges in law, in (1.4), to chordal \SLE_{\kappa(q)} from a to b in D.

  2. (ii)

    Under the specified free infinite-volume law, \Gamma_\delta converges in law as \delta\downarrow0 to the nested whole-plane \CLE_{\kappa(q)}, in the spherical collection topology just defined. The limit is Möbius invariant.

Both conclusions hold along every mesh sequence. No uniformity in q is asserted.

Corollary 1.2 (Combined finite-law parameter range)

In Self-dual random-cluster interfaces below one, 23 September 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

For this statement, fix q\in(0,4) and put

p(q)=\frac{\sqrt q}{1+\sqrt q}, \qquad \kappa(q)=\frac{4\pi}{\arccos(-\sqrt q/2)}.

Let D be a bounded Jordan domain with smooth simple boundary and distinct boundary marks a,b. Take simple nearest-neighbor lattice polygon approximations D_{\delta_n}, with \delta_n\downarrow0 and the full closed-polygon graphs specified above, and take a_{\delta_n},b_{\delta_n} to be distinct polygon vertices. Require counterclockwise parametrizations of \partial D_{\delta_n} converging uniformly on [0,1] to one of \partial D, all injective on [0,1), with the marks a_{\delta_n},b_{\delta_n} and a,b at parameters 0,1/2 respectively. Wire all vertices of the counterclockwise arc from b_{\delta_n} to a_{\delta_n}, including its endpoints, leaving the other boundary vertices singleton. Sample (1.2) with this q and p=p(q), and declare wired-arc boundary edges open for drawing. Then the prescribed medial strand, oriented from a_{\delta_n} to b_{\delta_n}, converges in law along the full mesh sequence to chordal \SLE_{\kappa(q)}(D;a,b) in (1.3). No uniformity in q is asserted.

The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.

Seven more possible matches

  • Theorem 1.1 in Quenched SLE Universality for Weakly Disordered FK–Ising Interfaces, 5 October 2026.
  • Theorem 1.1 (Below-one interface convergence) in Self-dual random-cluster interfaces below one, 23 September 2026.
  • Theorem 2.1 in Thermal FK–Ising interfaces and massive SLE, 5 October 2026.
  • Theorem 1.2 (Cardy’s formula for square-lattice bond percolation) in Conformal Limits of Critical Square-Lattice Random-Cluster Interfaces, 5 October 2026.
  • Theorem 1.2 (Cardy’s formula for square-lattice bond percolation) in Square-lattice FK interfaces and nested loops for 1 <= q < 4, 23 September 2026.
  • Theorem 1.1 in Natural Occupation Measures for Critical Square-Lattice FK Interfaces, 5 October 2026.
  • Corollary 1.3 (Square-bond arm and thermodynamic exponents) in Square-lattice FK interfaces and nested loops for 1 <= q < 4, 23 September 2026.
Reported proof verification
The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations
Six current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Square-lattice FK interfaces and nested loops for 1 <= q < 4

23 September 2026, current edition.

Read it herePDF

For every fixed \(1\le q\lt 4\), critical square-lattice random-cluster Dobrushin interfaces converge as ordered curves to chordal \(\mathop{\mathrm{SLE}}\nolimits _{\kappa(q)}\), where \(\kappa(q)=4\pi/\arccos(-\sqrt q/2)\), confirming the Rohde–Schramm prediction in this parameter range. This holds in every bounded Jordan domain under uniform marked boundary approximation. The complete nested plane loop collections converge to whole-plane \(\mathop{\mathrm{CLE}}\nolimits _{\kappa(q)}\) in a spherical matching topology retaining multiplicities and traversals. At q = 1 we obtain Cardy’s formula for square-lattice bond percolation with free boundary edges.

Self-dual random-cluster interfaces below one

23 September 2026, current edition.

Read it herePDF

For every fixed \(0\lt q\lt 1\), we prove that the Dobrushin interface of the square-lattice random-cluster model at its self-dual parameter converges to chordal SLEκ, where \(\kappa=4\pi/\arccos(-\sqrt q/2)\in(6,8)\). The approximating domains are simple closed nearest-neighbor lattice polygons with distinct marked vertices, whose marked boundary parametrizations converge uniformly to those of a bounded smooth Jordan domain. Convergence holds along the full mesh sequence in the uniform metric on oriented curves modulo increasing reparametrization. The proof combines finite connection comparisons below one, localization in irregular tiled disks, and a boundary observable that determines the limiting Loewner driver.

Thermal FK–Ising interfaces and massive SLE

5 October 2026, current edition.

Read it herePDF

We prove convergence of thermal FK–Ising interfaces, for every fixed nonzero mass of either sign, on uniformly angle-bounded isoradial lattices in bounded simply connected domains. The limit is independent of the lattice and the admissible domain approximation. For positive mass it is the unique massive SLE\(_{16/3}\) law with locally finite-energy drift prescribed by a massive boundary value problem; negative mass follows by duality and reversal. The theorem also allows Carathéodory approximations whose diameters diverge.

Natural Occupation Measures for Critical Square-Lattice FK Interfaces

5 October 2026, current edition.

Read it herePDF

We prove that the rescaled counting measure of a critical square-lattice Fortuin–Kasteleyn Dobrushin interface in the unit square converges to the Minkowski-content measure of its Schramm–Loewner limit, for every fixed cluster weight \(1\le q\lt 4\). A single deterministic constant times the predicted power of the mesh gives the normalization. Convergence is joint with the ordered curve and includes the total mass, giving the scaling limit of the interface’s total number of steps.

Conformal Limits of Critical Square-Lattice Random-Cluster Interfaces

5 October 2026, current edition.

Read it herePDF

For every fixed \(1\le q\le4\), critical square-lattice random-cluster Dobrushin interfaces converge to chordal \(\mathop{\mathrm{SLE}}\nolimits _{\kappa(q)}\), where \(\kappa(q)=4\pi/\arccos(-\sqrt q/2)\), and the complete nested plane loop collections converge to whole-plane \(\mathop{\mathrm{CLE}}\nolimits _{\kappa(q)}\). The results hold under uniform marked Jordan boundary approximation and retain loop multiplicities and traversals. At q = 1 we obtain Cardy’s formula for square-lattice bond percolation with free boundary edges.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Would win a Fields Medal”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

  • Family 223 No single paper statement clearly matches OpenAI’s description by wording, and no review identifying the intended theorem is recorded. Open the form

State the result in Lean

  • Family 223 The release has no Lean statement for this family. Open the form