Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

The geometric phase diagram, diffusion, and spectra of random planar maps

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

Critical Fortuin–Kasteleyn planar maps converge to Liouville quantum gravity spheres for \(0\lt q\le4\) and to the Brownian continuum random tree for q > 4, establishing the surface-to-tree geometric transition. For FK–Ising and spanning-tree-weighted maps, stationary random walks converge to Liouville Brownian motion on the limiting sphere. The FK–Ising spectral result also gives convergence of eigenvalues and heat traces, using the stated Brownian/LQG inputs. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments

What the papers state

Theorem 1.1

In Random Walks on Critical FK–Ising Maps and Liouville Brownian Motion, 5 October 2026

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

Let (M_n,A_n) have law (1.1), and let a_n>0 be any deterministic sequence with a_n\to0 such that

(V_n,a_nd_n,\mu_n)\ \Longrightarrow\ (S,D_h,\mu_h)

in Gromov–Hausdorff–Prokhorov law. Given the map, start r independent simple random walks X^{n,1},\ldots,X^{n,r} independently from \mu_n. Given h, start r independent Liouville Brownian motions B^{h,1},\ldots,B^{h,r} independently from \mu_h, with the convention (1.3). For every fixed integer r\ge1,

\left(\overline M_n,a_nd_n,\mu_n; (\overline X^{n,j}_{nt})_{t\ge0,\,1\le j\le r}\right) \ \Longrightarrow\ \left(S,D_h,\mu_h; (B^{h,j}_t)_{t\ge0,\,1\le j\le r}\right)

in the curve-decorated Gromov–Hausdorff–Prokhorov topology.

No Lean statement in the release is paired with this theorem.

Theorem 1.1 (Joint Liouville spectral limit)

In Spectral convergence for critical FK–Ising planar maps, 5 October 2026

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

The form (1.5) is closable on L^2(\mu_h). Its closure has compact resolvent, has the constants as its one-dimensional kernel, and satisfies H_h(t)<\infty for every t>0. As n\to\infty through all positive integers,

\left( (V_n,a_nd_n,\mu_n),\ (n\lambda_{n,j})_{j\ge0},\ H_n \right) \ \Longrightarrow\ \left( (\Sph,D_h,\mu_h),\ (\Lambda_j(h))_{j\ge0},\ H_h \right).

The first coordinate has the Gromov–Hausdorff–Prokhorov topology on isometry classes of compact metric probability spaces. The second has the product topology on [0,\infty]^{\N_0}. The third has C_{\mathrm{loc}}((0,\infty)), the topology of uniform convergence on each [\delta,T] with 0<\delta<T<\infty. All three limiting coordinates are constructed from the same quantum sphere h.

No Lean statement in the release is paired with this theorem.

Theorem 1.1 (The critical area-marked sphere)

In The critical Liouville quantum sphere and geometric limits of FK maps at q=4, 24 September 2026

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

As \gamma\uparrow2, the laws of (H_\gamma,\nu_\gamma) converge to a unique nondegenerate probability law \mathsf P_{\rm crit} in

H^{-1}(S^2,g_{\rm round})\times\mathcal P(S^2),

with the norm topology in the first factor and the weak topology in the second. Let (H,\nu) have this law and set h=H+\log g_{\rm round} in local conformal coordinates. Then \nu=\mu_h^{\rm crit}, where on compact sets avoiding 0,1,\infty,

\mu_h^{\rm crit}(\dd z) =\lim_{\eps\downarrow0} \bigl(2\log(1/\eps)-h_\eps(z)\bigr) \eps^2e^{2h_\eps(z)}\,\dd^2z

locally weakly in probability. This positive measure extends across the three marks without atoms, has full support, and has total mass one.

After forgetting the three marks, sampling three new conditionally independent area points and normalizing them to 0,1,\infty recovers \mathsf P_{\rm crit}. If f maps the new coordinate to the old one, the field transforms as

h_{\rm new}=h_{\rm old}\circ f+2\log|f'|.

With any one fixed deterministic normalization of the Ding–Gwynne critical local metric, the compatible chart metrics define an intrinsic length metric on the sphere punctured at the three marks. Its completion adds exactly those marks and is a finite continuous metric D_h on S^2, inducing the usual topology. The area and completed metric are measurable functions of the same field and obey the corresponding charge-2 coordinate rules.

No Lean statement in the release is paired with this theorem.

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.2 (Intrinsic spherical scaling; companion consequence) in Canonical conformal limits of subcritical FK planar maps, 24 September 2026.
  • Theorem 1.1 (Joint canonical limit) in Canonical conformal limits of subcritical FK planar maps, 24 September 2026.
  • Theorem 1.1 (Metric and measure convergence) in Metric-measure limits of subcritical FK and spanning-tree planar maps, 24 September 2026.
  • Theorem 1.2 (Joint critical universality) in The critical Liouville quantum sphere and geometric limits of FK maps at q=4, 24 September 2026.
  • Theorem 1.1 (Linear clock and conditional laws) in A Linear Clock for Random Walk on Tree-Weighted Planar Maps, 5 October 2026.
  • Corollary 1.3 (The compact metric-measure limit) in The critical Liouville quantum sphere and geometric limits of FK maps at q=4, 24 September 2026.
  • Theorem 1.1 in Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four, 24 September 2026.
Reported proof verification
One Lean statement in the release; two independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Seven 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.

Random Walks on Critical FK–Ising Maps and Liouville Brownian Motion

5 October 2026, current edition.

Read it herePDF

We prove that stationary random walks on critical spherical FK–Ising planar maps converge to Liouville Brownian motion on the ordinary unit-area \(\sqrt3\)-quantum sphere, using the geometric and electrical results of the spectral companion. The walk chooses uniformly among all incident half-edges, retaining loops and multiple edges. With the corner measure as the stationary law, the deterministic time acceleration is exactly the number of map edges. For any deterministic metric scale giving the metric-measure limit, convergence retains that same surface and any fixed finite number of conditionally independent walks with their time parameters.

Spectral convergence for critical FK–Ising planar maps

5 October 2026, current edition.

Read it herePDF

Using the conformal and metric-measure companion results and the stated Brownian/Liouville quantum gravity inputs, we prove spectral convergence for critical spherical FK–Ising maps to Liouville Brownian motion on the ordinary unit-area \(\sqrt3\)-quantum sphere. The discrete walk has total attempt rate one, uses every map edge including loops and multiplicities, and has the corner measure as its stationary law. Accelerating time by the number of map edges gives joint convergence of the metric-measure space, all ordered eigenvalues with multiplicities and padding, and the heat trace locally uniformly at strictly positive times. The conductivity and clock constant are one in these conventions.

A Linear Clock for Random Walk on Tree-Weighted Planar Maps

5 October 2026, current edition.

Read it herePDF

We prove that stationary random walk on a planar map sampled with weight equal to its number of spanning trees converges to Liouville Brownian motion on the unit-area \(\sqrt2\)-Liouville quantum sphere. The convergence retains the conditional path law jointly with the measured metric space. The walk chooses uniformly among all incident half-edges and starts from the stationary degree measure. For total attempt rate one and the continuum Dirichlet form with factor 1/2, the time acceleration is exactly the number of map edges. The result uses the companion contour and metric limits for this same ensemble.

Canonical conformal limits of subcritical FK planar maps

24 September 2026, current edition.

Read it herePDF

For every fixed \(0\lt q\lt 4\), we prove joint convergence of spherical Fortuin–Kasteleyn planar maps in their flag-triangle uniformization to the corresponding unit-area Liouville quantum gravity sphere decorated by an independent conformal loop ensemble. The convergence includes the area measure, deterministically rescaled graph distances between all vertex pairs, and the full nested interface collection, with interfaces converging uniformly up to reparameterization.

The critical Liouville quantum sphere and geometric limits of FK maps at q=4

24 September 2026, current edition.

Read it herePDF

We construct the field and area law of the unit-area critical Liouville quantum sphere as a limit of ordinary subcritical quantum spheres, and equip it with its critical intrinsic metric. We then prove that spherical Fortuin–Kasteleyn planar maps at q = 4, embedded by their equilateral flag uniformizations, converge jointly to this sphere decorated by an independent nested conformal loop ensemble CLE4. With deterministic distance normalization, the convergence includes the area measure, the full embedded distance function, and every macroscopic interface through all positive integer edge counts.

Metric-measure limits of subcritical FK and spanning-tree planar maps

24 September 2026, current edition.

Read it herePDF

We resolve the finite spherical cases of Gwynne and Miller’s graph-metric conjecture for critical Fortuin–Kasteleyn maps at each fixed \(q\in(0,4)\) and for uniform spanning-tree-decorated maps. After deterministic rescaling of graph distances, these maps, equipped with the vertex probability measure proportional to degree, converge in Gromov–Hausdorff–Prokhorov law to their ordinary unit-area Liouville quantum gravity spheres. Distances use every primal edge, and convergence holds through all positive integer edge counts.

Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four

24 September 2026, current edition.

Read it herePDF

We prove the finite-volume continuum-random-tree prediction for critical Fortuin–Kasteleyn planar maps at every fixed q > 4. After rescaling graph distances by a constant times n−1/2, an n-edge map with normalized degree measure converges to the Brownian continuum random tree in the Gromov–Hausdorff–Prokhorov topology. The convergence holds through all positive integer sizes.

One Lean statement in this family

Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

FKCRT

The paper states

The words they share: isometry, prokhorov, modulo, preserving, hausdorff, spaces, real, metric, probability, integers, measure, compact, brownian, tree, maps, limits, finite, gromov, 1/2, topology, constant, positive.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Brownian continuum-random-tree limit for finite FK maps

FKCRT.lean, the release lists it as a supporting statement.

def MainStatement : Prop :=  ∀ q : ℝ, 4 < q → ∃ c : ℝ, 0 < c ∧    ∀ (Ω : Type) (mΩ : MeasurableSpace Ω) (P : @Measure Ω mΩ),      @IsProbabilityMeasure Ω mΩ P →      ∀ B : Fin 3 → ℝ≥0 → Ω → ℝ,        (∀ i, @IsBrownianReal Ω mΩ (B i) P) →        @iIndepFun Ω (Fin 3) mΩ (fun _ => ℝ≥0 → ℝ) (fun _ => inferInstance)          (fun i ω t => B i t ω) P →        ∀ F : MetricMeasureData → ℝ, IsGHPTest F →          Tendsto (fun n : ℕ => finiteExpectation q (c / Real.sqrt (n + 1)) n F)            atTop (𝓝 (@brownianExpectation Ω mΩ P B F))theorem finite_fk_maps_converge_to_brownian_crt : MainStatement := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).

Their note: Only the q > 4 Brownian-CRT limit is stated: MainStatement : ∀ q > 4, ∃ c > 0,... Tendsto (fun n => finiteExpectation q (c / √(n+1)) n F) atTop (𝓝 (brownianExpectation P B F)) for every GHP-test F, with the standard excursion realized as the norm of three independent Mathlib IsBrownianReal bridges. Not stated: the 0 < q <= 4 convergence to Liouville quantum gravity spheres, the Liouville Brownian motion limits of random walks, and the FK-Ising spectral/heat-trace convergence (docs: ‘For every fixed q>4...’).

Definitions the group asks readers to compare with the paper: Entire topology is hand-rolled: MetricMeasureData, ghpEDist := ⨅ amalgamating pseudometrics on X ⊕ Y (Hausdorff/Lévy-Prokhorov), IsGHPTest F := (∃ C, ∀ X, |F X| ≤ C) ∧ ∀ X valid, ∀ ε, ∃ δ, ∀ Y valid, ghpEDist X Y < δ → |F Y - F X| < ε (convergence in distribution defined by bounded tests continuous at valid points); maps are pairs of dart permutations with fkWeight q M A := q^(k(A) + (|A| - |V|)/2); treeSpace is a quotient of unitInterval by excursionDist. Plausible and documented in the file header, but none of it is Mathlib’s notion.

“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).

The gap they name: LQG-sphere limits for 0<q<=4 (and the transition), random-walk convergence to Liouville Brownian motion for FK–Ising and tree-weighted maps, and FK–Ising spectral convergence; six of the seven manuscripts have no Lean statement

“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

For every fixed $q>4$, the formalization proves the Brownian continuum-random-tree limit for critical finite Fortuin–Kasteleyn planar maps. After rescaling graph distances in an $n$-edge map by a constant depending on $q$ times $n^{-1/2}$ and using normalized degree measure, the metric-measure space converges in distribution to the Brownian continuum random tree in the Gromov–Hausdorff–Prokhorov topology. The convergence holds through all positive integer sizes.

AI-drafted comparisons, with no recorded human review

  • Brownian continuum-random-tree limit for finite FK maps FKCRT

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for q > 4, critical finite Fortuin–Kasteleyn planar maps, with distances rescaled by c(q)n^{-1/2}, converge to the Brownian continuum random tree in the Gromov–Hausdorff–Prokhorov topology.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Brownian continuum-random-tree limit for finite FK maps FKCRT

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

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

This family’s papers cite no paper elsewhere in the release.

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

No paper elsewhere in the release cites this family’s papers.

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 explanationCompare the Lean statement with the paperSuggest 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 “Career-defining publication”. The page says that nothing on it is verified.

    Author not stated. Source

  • Nina Holden, The Tutte embedding of tree-weighted planar maps converges to Liouville quantum gravity, 7 October 2026. Source

    Holden says OpenAI’s linear-clock paper on tree-weighted planar maps is close to the Tutte-embedding result in this paper and solves several open problems listed in its future-directions section.

  • Nina Holden, Pu Yu, The circle packing and Riemann uniformization embedding of the tree-weighted planar maps converges to Liouville quantum gravity, 7 October 2026. Source

    Holden and Yu say that, to their knowledge, none of the OpenAI planar-map results imply their circle-packing convergence theorem, or the reverse.

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.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

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

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 211 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form