Critical SK autocorrelation processes and dynamics across the temperature transition
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
For zero-field Gaussian SK heat-bath dynamics with rate-one updates per spin, proves worst-start cutoff on the \(\log n\) scale for fixed \(0\le\beta\lt 1\), mixing time \(n^{2/3+o(1)}\) at β = 1, and stretched-exponential mixing from a Gibbs-sampled fixed starting configuration for β > 1, in probability over disorder. At criticality, rescaled stationary and quench autocorrelation processes have universal random limits for Gaussian and Rademacher disorder; the quench limit relaxes to the stationary limit. (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
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
Twelve other possible matches are listed below the card, among them Theorem 1.1 in A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase and Corollary 2(Two-sided typical-start bounds) in A typical-start upper bound for low-temperature SK Glauber dynamics.
There is a measurable family (h_s^g)_{s>0}, with h_s^g\in L^2(\Pi_g), such that for almost every g the following properties hold.
1.
For every s>0,h_s^g\ge0 and \Pi_g[h_s^g]=1. For s,t>0,
h_{s+t}^g=S_t^g h_s^g.
Moreover,
h_s^g\Pi_g\ \weakto\ \delta_0
\quad\text{in the product topology on }\R^\N
\quad(s\downarrow0),
\qquad
\|h_s^g-1\|_{L^1(\Pi_g)}\longrightarrow0
\quad(s\to\infty).
in C_{\mathrm{loc}}((0,\infty))
\times C_{\mathrm{loc}}((0,\infty)^2). The two coupling laws have the same g, the same family h^g, and the same coefficient c_*.
4.
For every 0<a<b<\infty,
\sup_{a\le t\le b}|B_g(s,t)-A_g(t)|
\longrightarrow0
\quad\text{in probability over }g
\quad(s\to\infty).
The positive-time density limits of the Gaussian dynamics with initial law \nu_n select this family, as made precise in Theorem 6.1. The normalization is exactly (1.2)–(1.3).
No Lean statement in the release is paired with this theorem.
Twelve more possible matches
Theorem 1.1in A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026.
Corollary 2(Two-sided typical-start bounds)in A typical-start upper bound for low-temperature SK Glauber dynamics, 24 September 2026.
Theorem 1.1(Critical mixing and functional inequalities)in Critical mixing in the Sherrington–Kirkpatrick model, 25 September 2026.
Theorem 1.1(Realized equilibrium initial states)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Corollary 1.2in Stretched-exponential barriers for typical SK initial states, 24 September 2026.
Theorem 1.1in Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026.
Theorem 1.1(Functional universality)in Functional universality of critical SK autocorrelations, 5 October 2026.
Theorem 1(Mixing from a typical Gibbs state)in A typical-start upper bound for low-temperature SK Glauber dynamics, 24 September 2026.
Theorem 1.2(Realized equilibrium starts and linear observables)in Critical mixing in the Sherrington–Kirkpatrick model, 25 September 2026.
Theorem 1.2(Covariance and linear tests)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Theorem 1.3(Critical mixing bounds)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Theorem 1.1in Stretched-exponential barriers for typical SK initial states, 24 September 2026.
Reported proof verification
Five Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
We prove joint functional convergence of the stationary and quench autocorrelations of zero-field Sherrington–Kirkpatrick heat-bath dynamics at inverse temperature β = 1, with the same random limit for Gaussian and Rademacher couplings. Each site has a rate-one clock, mean spin autocorrelations are multiplied by n1/3, and waiting times and lags are measured in units n2/3. The quench starts from independent fair spins, and convergence is uniform on compact sets of positive waiting times and lags. The quench limit is selected by these initial states and relaxes to the stationary limiting autocorrelation as the waiting time tends to infinity.
We prove that the stationary spin autocorrelation of the zero-field Sherrington–Kirkpatrick model at inverse temperature β = 1 has a common functional scaling limit for Gaussian and Rademacher couplings. With rate-one heat-bath clocks at every site, time is scaled by n2/3 and the mean spin autocorrelation is multiplied by n1/3. The functions converge in law uniformly on compact positive-time intervals. Their limiting law is not a point mass: it retains sample-to-sample randomness, and its functions decay to zero at large times.
For every fixed inverse temperature \(0\lt \beta\lt 1\), we prove that the unscaled spectral gap of single-site heat-bath dynamics for the zero-field Gaussian Sherrington–Kirkpatrick model is bounded away from zero with probability tending to one over the disorder. Equivalently, the Gibbs law satisfies a dimension-free Poincaré inequality for all functions.
We prove worst-case total-variation cutoff for the zero-field Gaussian Sherrington–Kirkpatrick heat-bath dynamics at every fixed inverse temperature \(0\leq\beta\lt 1\). With rate-one refresh at each spin, the cutoff location is \(\log n/(2\lambda(\beta))\) for a positive deterministic rate \(\lambda(\beta)\). The location for uniformly chosen single-site update attempts is n times as large. Convergence is in probability over the disorder.
At the critical inverse temperature β = 1, we prove slow mixing for zero-field Gaussian Sherrington–Kirkpatrick heat-bath dynamics from typical equilibrium configurations held fixed as initial states. For every deterministic sequence \(t_n=o(n^{2/3})\) in rate-one-per-site time, the Gibbs mass of initial states whose time-tn total-variation distance from equilibrium exceeds 1/4 tends to one in probability over the disorder. The same statement holds for every deterministic integer sequence \(k_n=o(n^{5/3})\) of uniform-site update attempts.
At every fixed inverse temperature β > 1, we prove a stretched-exponential obstruction to mixing for the zero-field Sherrington–Kirkpatrick model from typical equilibrium configurations held fixed as initial states. The Gibbs mass of states whose total-variation distance from equilibrium at time \(\exp(n^{1/10000})\) exceeds 1/4 tends to one in probability over the disorder. This holds for rate-one-per-site heat-bath dynamics and after the same stated number of discrete update attempts.
For every fixed inverse temperature β > 1, we prove subexponential mixing for rate-one-per-site heat-bath dynamics in the zero-field Gaussian Sherrington–Kirkpatrick model from a typical equilibrium configuration. If one Gibbs-sampled configuration is held fixed as the initial state, its total-variation distance from equilibrium is at most 1/4 by time \(\exp(n^{1-1/40000000})\), with joint probability tending to one over the disorder and the sampled state.
At the critical inverse temperature β = 1, we determine the worst-start total-variation mixing exponent for single-site heat-bath dynamics in the zero-field Gaussian Sherrington–Kirkpatrick model. The mixing time is \(n^{2/3+o(1)}\) when every site has rate one, or \(n^{5/3+o(1)}\) attempted uniform-site updates, in probability over the disorder.
Five Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
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.
CriticalSK
The paper states
No paper theorem is paired with this Lean statement.
no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.
Statements it shares words with:
Theorem 1.2(Realized equilibrium starts and linear observables)in Critical mixing in the Sherrington–Kirkpatrick model, 25 September 2026.
Theorem 1.1(Realized equilibrium initial states)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Corollary 2(Two-sided typical-start bounds)in A typical-start upper bound for low-temperature SK Glauber dynamics, 24 September 2026.
Theorem 1(Mixing from a typical Gibbs state)in A typical-start upper bound for low-temperature SK Glauber dynamics, 24 September 2026.
Proposition A.2(A two-spin example)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Proposition A.1(Arbitrary refresh times)in Critical slowing down in the Sherrington–Kirkpatrick model, 24 September 2026.
Proposition 9.12(Cutoff for single-site update attempts)in Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026.
Proposition 13.6(Terminal extension, uniformly in the initial spin law)in Critical mixing in the Sherrington–Kirkpatrick model, 25 September 2026.
CriticalSK.lean, the release lists it as a main result.
theoremrealized_equilibrium_initial_states : (∀ t : ℕ → ℝ, (∀ n, 0 ≤ t n) → Tendsto (fun n => t n / (n : ℝ) ^ ((2 : ℝ) / 3)) atTop (𝓝 0) → ∀ δ : ℝ, 0 < δ → Tendsto (fun n => (disorderLaw n {W | δ ≤ |continuousGoodMass W (t n) - 1|}).toReal) atTop (𝓝 0)) ∧ (∀ k : ℕ → ℕ, Tendsto (fun n => (k n : ℝ) / (n : ℝ) ^ ((5 : ℝ) / 3)) atTop (𝓝 0) → ∀ δ : ℝ, 0 < δ → Tendsto (fun n => (disorderLaw n {W | δ ≤ |discreteGoodMass W (k n) - 1|}).toReal) atTop (𝓝 0)) := bysorry
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”.
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.
Consequently both \PP\{T^J(x_0)>n^a\} and \PP\{T_{\mathrm{disc}}^J(x_0)>n^a\} tend to one under the same joint law. Each assertion is equivalently a statement that the Gibbs mass of the indicated initial states tends to one in probability over J.
The words they share: gibbs, 1/4, mass, time, law, pi, obstruction, initial, states, tend, beta, one, probability.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
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.
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.
SKRatio.lean, the release lists it as a supporting statement.
theoremratio_cutoff (β ε η : ℝ) (hβ0 : 0 ≤ β) (hβhalf : β < 1 / 2) (hε0 : 0 < ε) (hεhalf : ε < 1 / 2) (hη : 0 < η) : Tendsto (fun n : ℕ => disorderLaw β n {g : Disorder n | 1 + η < (mixingTime g ε : ℝ) / (mixingTime g (1 - ε) : ℝ)}) atTop (𝓝 0) ∧ (∀ᶠ n : ℕ in atTop, ∀ g : Disorder n, 0 < mixingTime g (1 - ε)) := bysorry
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.
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:Stated: stretched-exponential barrier for β > 1 (SK.main : Tendsto continuousBadMass atTop (𝓝 1) ∧ Tendsto discreteBadMass atTop (𝓝 1) at time exp(n^(1/10000)), expected bad Gibbs mass over disorder); high-temperature spectral gap sk_main (0<β<1: Poincaré constant C and gap ≥ 1/(Cn)) as a supporting result; ratio cutoff ratio_cutoff only for 0 ≤ β < 1/2. Critical case is one-sided: critical_mixing_bounds gives n^(2/3-ε) ≤ continuousMixingTime ≤ exp(εn) (discrete n^(5/3-ε) ≤... ≤ exp(εn)), so the headline ‘mixing time n^{2/3+o(1)} at β=1’ has no n^{2/3+ε} upper bound in Lean. Not stated: cutoff for 1/2 <= β < 1 and its log n location, and the critical autocorrelation-process limits (Gaussian/Rademacher, quench relaxing to stationary).
Definitions the group asks readers to compare with the paper:Custom ‘mixing time’: continuousMixingTime W := sInf {t | 0 ≤ t ∧ ∀ x, continuousDistance W t x ≤ 1/4} (matrix exponential kernel NormedSpace.exp (t • generator W)), discreteMixingTime W := sInf {k : ℕ | ∀ x, discreteDistance W k x ≤ 1/4}, SKRatio.mixingTime g ε := sInf {k | discreteDistance g k ≤ ε}: standard worst-start total-variation mixing (sets are nonempty so sInf is a true min), but hand-written; SKBarriers uses its own heatBath kernel and a Poissonized continuousKernel (series in k).
“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.
cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).
The gap they name:Not stated: the critical autocorrelation universality (clause 4, the titular result); the n^{2/3+o(1)} upper bound at β = 1; the stretched-exponential upper bound for β > 1; cutoff for 1/2 ≤ β < 1, its log n location and continuous time (this last part is declared). Stated: the high-temperature spectral gap (supporting), discrete ratio cutoff for β < 1/2, critical lower bounds with an e^{εn} upper bound, the β > 1 barrier, and critical covariance/linear-test scaling.
“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.
For every fixed inverse temperature $0<\beta<1$, the formalization proves a dimension-independent Poincaré inequality for the zero-field Gaussian Sherrington–Kirkpatrick model with probability tending to one over the disorder. Equivalently, the unscaled single-site heat-bath spectral gap stays bounded away from zero. For dynamics that choose one site uniformly at each discrete step, the spectral gap is at least $1/(Cn)$ with probability tending to one, for a constant $C$ depending on $\beta$.
The formalized supporting result proves ratio cutoff for discrete single-site heat-bath dynamics in the zero-field Gaussian Sherrington–Kirkpatrick model for $0\le\beta<1/2$. For every $0<\varepsilon<1/2$ and $\eta>0$, the probability over the disorder that $t_{\mathrm{mix}}(\varepsilon)/t_{\mathrm{mix}}(1-\varepsilon)>1+\eta$ tends to zero as $n\to\infty$. The denominator is positive for all sufficiently large sizes.
The paper’s full range $\beta<1$, explicit cutoff location, and continuous-time conclusion are outside this selected statement.
At criticality in the zero-field Sherrington–Kirkpatrick model, the formalization proves that for every fixed $\varepsilon>0$, the continuous-time mixing time lies between $n^{2/3-\varepsilon}$ and $e^{\varepsilon n}$, and the discrete-time mixing count lies between $n^{5/3-\varepsilon}$ and $e^{\varepsilon n}$, with probability tending to one over the Gaussian disorder. The disorder has independent off-diagonal entries of variance $1/n$. Continuous updates have rate one per site; discrete time counts uniformly chosen single-site update attempts. Mixing is worst-start total variation at threshold $1/4$, with holding allowed.
For deterministic times $t_n=o(n^{2/3})$ or update counts $k_n=o(n^{5/3})$, the Gibbs mass of realized starting states still farther than $1/4$ from equilibrium tends to one in probability. For every deterministic positive sequence $M_n\to\infty$, the covariance operator norm and the linear Rayleigh supremum, using the unscaled heat-bath Dirichlet form, both lie between $n^{2/3}/M_n$ and $M_n n^{2/3}$ with probability tending to one. The covariance result does not give an upper bound for the full inverse spectral gap.
The formalization proves a stretched-exponential mixing obstruction for the zero-field Sherrington–Kirkpatrick model at every fixed inverse temperature $\beta>1$. At time $\exp(n^{1/10000})$, the expected Gibbs mass of initial configurations whose total-variation distance from equilibrium exceeds $1/4$ tends to one. Since this mass lies in $[0,1]$, it also tends to one in probability over the disorder.
The result covers both rate-one-per-site continuous-time heat-bath dynamics and the same stated number of discrete update attempts.
AI-drafted comparisons, with no recorded human review
Equilibrium starts, covariance, and mixing lower boundsCriticalSK
Unreviewed AI draft: states a paper’s theorem as the paper does. States the critical paper’s theorems on realised equilibrium starts and on covariance and linear tests at scale n^{2/3}, with the mixing lower bounds. The covariance result gives no upper bound for the inverse spectral gap.
Critical SK mixing boundsCriticalSKMixing
Unreviewed AI draft: states a paper’s theorem as the paper does. States the critical-slowing-down paper’s mixing bounds at β = 1: continuous-time mixing between n^{2/3−ε} and e^{εn}, and discrete counts between n^{5/3−ε} and e^{εn}, with probability tending to one.
Stretched-exponential barriers from typical equilibrium initial statesSKBarriers
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the barriers paper: for β > 1, at time exp(n^{1/10000}) most equilibrium starting states are still farther than 1/4 from equilibrium.
Spectral-gap bound throughout the high-temperature SK phaseSKHighTemperature
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for 0 < β < 1, a dimension-free Poincaré inequality for the SK Gibbs measure with probability tending to one, equivalently a spectral gap bounded away from zero.
Discrete mixing-time ratio cutoff for $\beta<1/2$SKRatio
Unreviewed AI draft: states a weaker form of a paper’s theorem. States ratio cutoff, t_mix(ε)/t_mix(1 − ε) → 1 in probability, for discrete dynamics and β < 1/2 only, which the note calls supporting. The cutoff theorem of the paper covers every β < 1 with an explicit cutoff location and continuous time.
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.
Equilibrium starts, covariance, and mixing lower boundsCriticalSK
Three reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original 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.
These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
Lemma E.3 and Table 2 of Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026
Reported by
cert-machine
Method
Exact computation
Their verdict
“CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: Lemma rcut:lem:scalar-data and Table rcut:tab:scalar-intervals of the appendix route (the independent beta < 1/2 proof) - the 205 quadrature terms, every finite enclosure, the whole error budget and every interval bound recomputed by the appendix’s directed integer recipe; the trapezoid lemma, strip holomorphy and beta-monotonicity are read, not run, and the cutoff headline (all beta < 1) is proved elsewhere in the paper by a different argument”
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.
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.
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside 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.
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.
jnshi, jnshi/math-lineage: precedence reviews of missing attributions in openai/math, 8 October 2026. Source
Two precedence reviews published listing earlier papers used without citation in family 227 manuscripts.
jnshi, jnshi/math-lineage: precedence reviews of missing attributions in openai/math, 8 October 2026. Source
An agent-run precedence review of the critical-mixing SK paper lists 12 earlier works whose techniques it uses without citation (9 unattributed reuse, 2 same-problem precedence, 1 structural), each with locators in both papers, for example the El Alaoui, Montanari and Sellke planted stochastic-localization framework.
jnshi, jnshi/math-lineage: precedence reviews of missing attributions in openai/math, 8 October 2026. Source
An agent-run precedence review of the high-temperature SK spectral-gap paper lists 8 earlier works used without citation (7 unattributed reuse, 1 same-problem precedence), including Kac-Rice complexity methods for TAP critical points, each with locators in both papers.
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
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
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
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
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 227The 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
Address a question raised in an independent assessment
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition 9.12 (Cutoff for single-site update attempts)
In Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026
How it was found
Its words were compared with the words of the Lean statement CriticalSKMixing.
Words they share
total, variation, spin, site, disorder, update, attempts, worst, single, one, probability
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Theorem 1.1 (Critical mixing and functional inequalities)
In Critical mixing in the Sherrington–Kirkpatrick model, 25 September 2026
How it was found
Its words were compared with the words of the Lean statement CriticalSKMixing.
Words they share
5/3, critical, mix, 2/3, 1/2, gaussian, disorder, varepsilon, probability
Review
Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
Their term
“partial”
What their term means
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. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
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; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator with Lean’s kernel: accepted (the check took 575 s; peak memory 6.5 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
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.
Lemma E.3 and Table 2 of Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 24 September 2026
Exact calculations for finite claims, cert-machine
Their verdict
“CERTIFIED”
Claim tested or proved
Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: Lemma rcut:lem:scalar-data and Table rcut:tab:scalar-intervals of the appendix route (the independent beta < 1/2 proof) - the 205 quadrature terms, every finite enclosure, the whole error budget and every interval bound recomputed by the appendix’s directed integer recipe; the trapezoid lemma, strip holomorphy and beta-monotonicity are read, not run, and the cutoff headline (all beta < 1) is proved elsewhere in the paper by a different argument”
Equilibrium starts, covariance, and mixing lower bounds
Role
the release lists it as a main result
Paired with
No paper theorem is paired with this Lean statement.
Who ran the proof-verification program
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.