Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Conformal universality for weakly interacting and random-bond Ising models

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

Weak finite-range square-symmetric even multispin perturbations of the square-lattice Ising model preserve critical bulk spin and energy limits; weak square-symmetric contour interactions also yield chordal SLE3 interface limits. With sufficiently weak iid bond disorder of any fixed bounded nondegenerate mean-zero law, critical spin interfaces converge to the same law in probability over environments. (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 a supporting step or a different result. Read the assessments

What the papers state

Theorem 1.1

In Quenched SLE₃ limits for general weak random-bond Ising models, 5 October 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

For every law \rho satisfying (1.1), there exists \varepsilon_0(\rho)>0 with the following property. Fix 0<\varepsilon<\min\{1,\varepsilon_0(\rho)\}. For every bounded Jordan domain D, distinct a,b\in\partial D, and deterministic square-lattice approximations satisfying (1.4) with \delta_n\downarrow0, the interface law at \beta=\beta_c^\rho(\varepsilon) satisfies

d_{\rm BL}(Q_{n,\omega},\mathsf S_{D;a,b}) \xrightarrow[n\to\infty]{\Prob_\rho}0.

The disorder threshold depends on \rho and not on D, its marked points, or the approximation sequence. Moreover, \beta_c^\rho(\varepsilon)=\tfrac12\log(1+\sqrt2)+O_\rho(\varepsilon^2).

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

Theorem 1.2 (Finite conditional resolution)

In Buffered comparison and stopping-band resolution in critical Ising, 23 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

Fix the preceding band geometry and use the critical plus-boundary law in a larger reference square. For every \epsilon,\eta>0, one can choose contour levels in any prescribed separated subwindows, a finite descriptor Z^\delta\in\{0,1,\ldots,m\}, and regular signed barriers \Gamma_1,\ldots,\Gamma_m with the following properties for all sufficiently fine meshes.

The exceptional state 0 has probability at most \epsilon. For every transcript in a good state i\in\{1,\ldots,m\}, insert the plus pins of \Gamma_i and then its minus pins. The sum of the two resulting total-variation changes on the target is at most \eta. The final target-side law Q_{i,\delta} is the same for every transcript in that state. Consequently this conclusion holds simultaneously for all bounded target observables, including mesh-dependent observables. For any fixed finite list of bands the descriptors have convergent joint laws.

The finite list of barriers and its positive geometric clearances are chosen before the mesh threshold. If another law has band density at most K times the reference density, its exceptional probability is at most K\epsilon.

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

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

Five more possible matches

  • Theorem 1.1 (Conformal universality) in Conformal universality of bulk Ising correlations under weak interactions, 23 September 2026.
  • Theorem 1.1 in SLE3 universality for weak finite-range Ising interactions, 23 September 2026.
  • Theorem 1.1 in Logarithmic Relative Fluctuations in the Weakly Disordered Planar Ising Model, 5 October 2026.
  • Theorem 1.2 (Quenched interface universality) in Quenched SLE₃ Universality for the Weak Random-Bond Ising Model, 5 October 2026.
  • Theorem 1.1 (Finite-graph comparison) in Buffered comparison and stopping-band resolution in critical Ising, 23 September 2026.
Reported proof verification
One Lean statement in the release; three independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Six current papers, each readable here as a page beside its PDF. One explanation by others.

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.

Quenched SLE₃ limits for general weak random-bond Ising models

5 October 2026, current edition.

Read it herePDF

For the planar Ising model with bonds \(J_e=1+\varepsilon\xi_e\), where the ξe have any fixed bounded, nondegenerate, mean-zero iid law, we prove quenched chordal SLE3 convergence for sufficiently small ε > 0. The temperature is the spontaneous-magnetization threshold. Convergence holds in probability over environments for the full oriented curve law in deterministic Jordan-domain approximations.

Quenched SLE₃ Universality for the Weak Random-Bond Ising Model

5 October 2026, current edition.

Read it herePDF

We prove quenched chordal SLE3 convergence for the planar Ising model with sufficiently weak independent symmetric two-valued ferromagnetic bonds. The temperature is the critical point defined by spontaneous magnetization. Convergence holds in probability over environments for the full oriented curve law in deterministic Jordan-domain approximations.

Logarithmic Relative Fluctuations in the Weakly Disordered Planar Ising Model

5 October 2026, current edition.

Read it herePDF

Assuming the stated deterministic critical-reference estimates, we prove that the relative second moment of the quenched critical spin correlation in the square-lattice Ising model with independent fair bonds \(1\pm\varepsilon\) grows as \((\log r)^{1/4+o(1)}\) for each sufficiently small fixed ε > 0. The correlation is evaluated at the physical critical temperature, with the thermodynamic limit taken before the disorder moments and the large-distance limit.

Conformal universality of bulk Ising correlations under weak interactions

23 September 2026, current edition.

Read it herePDF

We prove conformal universality of mixed bulk spin and energy correlations for the square-lattice Ising model with sufficiently small, square-symmetric, finite-range even multispin perturbations of either sign. One critical-temperature branch and two field normalizations apply in every bounded simply connected C2 Jordan domain with free, plus, or minus boundary conditions, and in the periodic thermodynamic plane state. Energies are centered in their actual states.

SLE3 universality for weak finite-range Ising interactions

23 September 2026, current edition.

Read it herePDF

We prove that every sufficiently small, square-symmetric finite-range perturbation of the planar Ising contour energy has a domain-independent inverse temperature at which its spin interface converges to chordal SLE3. The result allows interactions of either sign, arbitrary admissible exterior contours, and uniformly approximated Jordan domains. Convergence holds for the full oriented curve law in uniform distance modulo increasing reparametrization.

Buffered comparison and stopping-band resolution in critical Ising

23 September 2026, current edition.

Read it herePDF

We prove pointwise comparison and finite stopping-band approximation theorems for the critical nearest-neighbor Ising model on the square lattice. Arbitrary common pinned spins are allowed in the comparison: the likelihood ratio is controlled by a zero-field FK connection probability on the graph with those vertices deleted. For an interface exploration across a band of fixed positive width, finitely many regular signed barriers approximate every good conditional target law in total variation, uniformly over bounded observables and sufficiently fine meshes.

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. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.

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.

BufferedIsing

The paper states

Theorem 1.1 (Finite-graph comparison)

In Buffered comparison and stopping-band resolution in critical Ising, 23 September 2026

For every two configurations b,b' on J and every configuration a on I,

e^{-4\operatorname{arctanh}q_0} \leq \frac{\mu(\sigma_I=a\mid\sigma_J=b,\sigma_F)} {\mu(\sigma_I=a\mid\sigma_J=b',\sigma_F)} \leq e^{4\operatorname{arctanh}q_0}.

Either conditional law may be replaced by an arbitrary mixture of these laws. The bound is symmetric in the two terminal sets.

The words they share: arbitrary, comparison, conditional, configurations, finite, graph, laws, mixture, terminal.

Possible Lean counterpart

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

Finite-graph buffered Ising likelihood comparison

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

theorem finite_graph_comparison {n m : ℕ} (G : FiniteGraph n m)    (h : Fin n → ℝ) (I J F : Finset (Fin n))    (hIJ : Disjoint I J) (hIF : Disjoint I F) (hJF : Disjoint J F)    (i j : KeptVertex F) (hi : i.val ∈ I) (hj : j.val ∈ J)    (a τ : Spins n) (mix mix' : Spins n → ℝ)    (hmix : ∀ b, 0 ≤ mix b) (hmix' : ∀ b, 0 ≤ mix' b)    (hmixsum : ∑ b, mix b = 1) (hmix'sum : ∑ b, mix' b = 1) :    Real.exp (-4 * Real.artanh (qZero G I J F i j)) ≤        mixtureProb G h I J F a τ mix / mixtureProb G h I J F a τ mix' ∧      mixtureProb G h I J F a τ mix / mixtureProb G h I J F a τ mix' ≤        Real.exp (4 * Real.artanh (qZero G I J F i j)) := 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.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

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 a supporting result (their term: “supporting-only”).

Their note: The only statement is a technical finite-graph inequality: finite_graph_comparison : exp(-4 * artanh (qZero..)) ≤ mixtureProb.. mix / mixtureProb.. mix' ∧... ≤ exp(4 * artanh (qZero..)) for Ising with arbitrary fields and boundary mixtures (docs: 'The paper’s finite stopping-band approximation theorem is outside this selected statement'). None of the headline results (universality of critical bulk spin/energy limits under weak multispin perturbations, SLE_3 interface limits, weak iid bond disorder) is stated.

“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.

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 different result (their term: “DIFFERENT”).

The gap they name: None of the headline’s three claims (bulk conformal universality, SLE₃ interface limits for contour perturbations, quenched SLE₃ for weak random bonds) is stated. The family’s only challenge is a finite-graph Ising likelihood-ratio inequality — a proof ingredient from one of the family’s six manuscripts (‘Buffered comparison and stopping-band resolution in critical Ising’). It neither implies the headline nor is implied by it, and it is not among the supporting results declared in ComparatorChallenges/README.md.

“DIFFERENT”, in their words: The challenge statements state a different theorem from the headline.

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

The formalized result compares conditional Ising probabilities on finite graphs when two boundary mixtures differ but a common set of spins is pinned. If $q_0$ is the associated zero-field Fortuin–Kasteleyn connection probability after deleting the pinned vertices, the likelihood ratio lies between $\exp(-4\mathrm{artanh}\,q_0)$ and $\exp(4\mathrm{artanh}\,q_0)$. The statement allows arbitrary external fields and arbitrary probability mixtures satisfying the stated disjointness conditions. The paper’s finite stopping-band approximation theorem is outside this selected statement.

AI-drafted comparisons, with no recorded human review

  • Finite-graph buffered Ising likelihood comparison BufferedIsing

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s finite-graph comparison theorem: conditional Ising likelihood ratios lie between exp(∓4 artanh q₀). The stopping-band resolution theorem is outside the statement.

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.

Finite-graph buffered Ising likelihood comparison BufferedIsing

Three 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
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 76 s; peak memory 6.2 GiB).10 October 2026Original report

Explanations by others

Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.

  • seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source

    Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.

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.

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 “Solid publication, could lead to tenure”. 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.

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 218 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Compare the proposed paper and Lean matches

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