OpenAI claim summary for Math-2913

Stretched-exponential mixing barriers for typical low-temperature SK starts

OpenAI's claim

OpenAI presents a proof in the selected manuscript. For each fixed $\beta>1$, typical SK equilibrium configurations held as starts are claimed to remain unmixed until at least $\exp(n^{1/10000})$.

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 fixed $\beta>1$, sample $x_0$ from $\pi_{n,\beta}^J$ and then use its realized value as the initial state. With $d^J(x,t)$ and $d_{\mathrm{disc}}^J(x,k)$ the corresponding total-variation distances, and $\kappa=1/10000$, \[ \mathbb P_{J,x_0\sim\pi}\{d^J(x_0,e^{n^\kappa})>1/4\}\to1,\qquad \mathbb P_{J,x_0\sim\pi}\{d_{\mathrm{disc}}^J(x_0,\lfloor e^{n^\kappa}\rfloor)>1/4\}\to1. \] The probability averages the interactions and the initial Gibbs sample; each transition-law distance holds the sample fixed.

Outline of the argument

Quantitative Parisi and constrained-overlap bounds produce a locked overlap sign around a reference sample. Disorder rotation and narrow-annulus coverage control rare sign-passage paths over the stretched-exponential horizon; spin reversal gives an equilibrium half-space that those paths cannot reach.

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, Stretched-exponential barriers for typical SK initial states, 2026-09-24; citation key OAI:Stretched-exponential-barriers-for-typical-SK-initial-states-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.