Glauber cutoff throughout the high-temperature SK phase

Glauber cutoff throughout the high-temperature SK phase

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Worst-start SK heat-bath dynamics is claimed to cut off at $(2\lambda(\beta))^{-1}\log n$ for each fixed $0\leq\beta<1$ in per-site rate-one time.

Mathematical statement of the claimed result

Result 1.

For independent standard Gaussian $J_{ij}$, $i<j$, with $J_{ji}=J_{ij},J_{ii}=0$, use the zero-field SK measure \[ \pi_{n,\beta}^J(x)=Z^{-1}\exp\left(\frac\beta{\sqrt n}\sum_{i<j}J_{ij}x_ix_j\right),\qquad x\in\{-1,1\}^n. \] Continuous heat-bath dynamics refreshes every site at rate one; a discrete step refreshes one uniformly selected site, including attempts that retain its spin. For every fixed $0\le\beta<1$, there is a deterministic $\lambda(\beta)>0$. Set $t_n=\log n/[2\lambda(\beta)]$, let $d_n(t)$ be the maximum continuous-time distance over initial states, and define $d_n^{\mathrm{disc}}(k)$ analogously. For every $0<\epsilon<1$, in disorder probability, \[ d_n((1-\epsilon)t_n)\to1,\quad d_n((1+\epsilon)t_n)\to0, \] \[ d_n^{\mathrm{disc}}(\lfloor(1-\epsilon)nt_n\rfloor)\to1,\quad d_n^{\mathrm{disc}}(\lceil(1+\epsilon)nt_n\rceil)\to0. \] The rate obeys $\lambda(0)=1$ and $0<\lambda(\beta)\le(1-\beta)^2$ for $0<\beta<1$; its definition through an equilibrium gradient operator is implicit. Temperature is fixed before $n\to\infty$.

Outline of the argument

Finite-path Gaussian calculus and projected likelihoods identify the equilibrium spin spectral decay. The proof makes one sufficiently long comparison block uniform over initial configurations before iterating it, allowing equilibrium information to control logarithmic-time worst-start total variation.

Formal verification

For family 227, the selected statements include the high-temperature gap for $\beta<1$, cutoff ratios only for $\beta<1/2$, critical lower mixing scales with a subexponential upper bound, and low-temperature barriers. They do not provide the full critical exponent, the full cutoff location, or the newer autocorrelation limits. The listed Comparator files are CriticalSK.lean, CriticalSKMixing.lean, SKBarriers.lean, SKHighTemperature.lean, SKRatio.lean. Named declarations include OAI.CriticalSK.covariance_and_linear_tests, OAI.CriticalSK.critical_mixing_bounds. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase, 2026-09-24; citation key OAI:Cutoff-throughout-the-high-temperature-Sherrington-Kirkpatrick-phase-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 227: Lean scope.
• Comparator CriticalSK.json.
• Comparator CriticalSK.lean.
• Comparator CriticalSKMixing.json.
• Comparator CriticalSKMixing.lean.
• Comparator SKBarriers.json.
• Comparator SKBarriers.lean.
• Comparator SKHighTemperature.json.
• Comparator SKHighTemperature.lean.
• Comparator SKRatio.json.
• Comparator SKRatio.lean.
• OpenAI catalogue entry.