Glauber dynamics of the Sherrington–Kirkpatrick model

Glauber dynamics of the Sherrington–Kirkpatrick model concerns how fast single-site heat-bath (Glauber) dynamics brings the Sherrington–Kirkpatrick spin glass to equilibrium, and how this changes across the equilibrium transition at inverse temperature β = 1. A family of manuscripts dated 24 and 25 September and 5 October 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims results in all three regimes for the zero-field Gaussian model: a spectral gap and cutoff at high temperature, the mixing exponent 2/3 at criticality, and stretched-exponential mixing from typical equilibrium starts at low temperature, together with universality of critical autocorrelation processes. The collection includes Lean formalizations of several of these statements. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase:
  • Aizenman, Lebowitz and Ruelle showed that the free energy per spin takes its annealed value throughout the high-temperature range β < 1. Wu proved a Poincaré inequality under a Dobrushin-type condition, and Bauerschmidt and Bodineau a high-temperature logarithmic Sobolev inequality for a different Dirichlet form.
  • For the heat-bath gap, Eldan, Koehler and Zeitouni reached β < 1/4; Anari, Jain, Koehler, Pham and Vuong proved O(n log n) mixing there, and Anari, Koehler and Vuong extended this to β up to about 0.295. Wang proved O(n log(n/ε)) mixing for every β < 1/2, and Boban, Li and Oveis Gharan a constant unscaled gap for β < 1/2 + ε₀.
  • Covariance estimates already cover all β < 1 (El Alaoui and Gaitonde; Brennecke, Schertzer, Xu and Yau); the manuscript's method transfers a functional inequality along stochastic localization (Eldan; El Alaoui and Montanari; Chen and Eldan).
• At criticality, Critical slowing down in the Sherrington–Kirkpatrick model recalls that the overlap of two equilibrium replicas has scale n^−1/3 at β = 1, against n^−1/2 at each fixed β < 1 (Du and Huang).

The original results

• Claims.
  • High temperature. For every fixed 0 < β < 1 the unscaled heat-bath spectral gap stays bounded away from zero with probability tending to one over the disorder, a dimension-free Poincaré inequality for all functions. For every fixed 0 ≤ β < 1 there is worst-start total-variation cutoff at time log n/(2λ(β)) for a positive deterministic rate λ(β).
  • Criticality. At β = 1 the worst-start mixing time is n^2/3+o(1) with rate-one clocks, or n^5/3+o(1) single-site update attempts. Most equilibrium configurations, fixed as initial states, are still far from equilibrium at times of order o(n^2/3). The rescaled stationary and quench autocorrelation processes have universal random limits for Gaussian and Rademacher disorder, and the quench limit relaxes to the stationary one.
  • Low temperature. For every fixed β > 1, a configuration sampled from the Gibbs measure and held fixed as the initial state is still at total-variation distance greater than 1/4 at time exp(n^1/10000), with probability tending to one; it is within 1/4 by time exp(n^{1−1/40000000}).
• Sources (openai/math repository, commit 1581d4c):
  • A spectral gap throughout the high-temperature Sherrington–Kirkpatrick phase;
  • Cutoff throughout the high-temperature Sherrington–Kirkpatrick phase;
  • Critical slowing down in the Sherrington–Kirkpatrick model;
  • Critical mixing in the Sherrington–Kirkpatrick model;
  • Stretched-exponential barriers for typical SK initial states;
  • A typical-start upper bound for low-temperature SK Glauber dynamics;
  • Universality of critical quench autocorrelations in the Sherrington–Kirkpatrick model;
  • Functional universality of critical SK autocorrelations.
• Formalization, as described by the repository. The scope note lists five Comparator statements: the high-temperature spectral gap (SKHighTemperature.lean); ratio cutoff for discrete dynamics for 0 ≤ β < 1/2 only (SKRatio.lean); at criticality, mixing times between n^2/3−ε and e^εn (CriticalSKMixing.lean) and the equilibrium-start, covariance and lower-bound statements (CriticalSK.lean); and the low-temperature barrier at exp(n^1/10000) (SKBarriers.lean). It states that the paper's full range β < 1, the cutoff location and the continuous-time cutoff are outside the selected statement.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 21 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates this family "partial" and records Comparator passes for all five challenges. Its note states that the critical case is one-sided in Lean (the upper bound is eεn, so the headline exponent 2/3 has no matching Lean upper bound), that cutoff is formalized only for β < 1/2 and without its location, and that the critical autocorrelation limits are not stated. It also notes that the mixing times are hand-written definitions.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10	cert-machine, openai/math lane K: runs 38019899278 (SKRatio), 38040214623 (SKBarriers, SKHighTemperature, CriticalSKMixing) and 38051470892 (CriticalSK)	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept all five solutions, in 449 to 8,967 s. The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal lists SKRatio among the challenges that con-leche accepts and Lean's official kernel did not finish within one hour; its table of exceptions does not list the other four challenges, so they were accepted by both.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee reviews of seven of the eight manuscripts (109, 121, 181, 192, 264, 288, 452) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap in any of the seven. Four reviews add a minor note on coverage or dependence: the quench-universality review spot-checked, but did not verify line by line, the technical sections carrying most of the weight; the cutoff review states that the uniformity over disorder-dependent initial laws is proved by contradiction through long limit constructions written at high compression; the functional-universality review states that key inputs come from companion manuscripts it could not check; the typical-start upper-bound review states that the argument depends on Lopatto's full replica-symmetry-breaking theorem for every β > 1, which it did not verify.	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-20	P. M. Aronow and Patrick Lopatto, Lower and Upper Bounds for Glauber Dynamics from Typical States of the Low-Temperature Sherrington–Kirkpatrick Model, pmaronow/fluctuations-palomar (GitHub; commit 2fd7036)	Extension (exponents; formal)	For every fixed β > 1 and every 0 < ω < 1/4, the time to reach total-variation distance 1/4 from a Gibbs-sampled initial state satisfies Aβn7/30 < log T ≤ n1−ω with probability tending to one, for both clocks, against the manuscripts' exponents 1/10000 and 1 − 1/40000000. The proofs follow the manuscripts' architecture, adding a three-replica comparison with the authors' n−7/10 mean-bias bound for the lower bound. Both bounds are formalized in Lean; the repository also formalizes the fluctuation-scale theorem listed on the page The low-temperature Sherrington–Kirkpatrick fluctuation law.	Manuscript and a Palomar submission package (statements, proofs and Comparator configuration); no registry entry for it was found on 21 October 2026.

Notes

• The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.