Probability and statistical mechanics · Result 234

All-temperature pressure of orthogonally invariant Ising spin glasses

1 paperLean

Gives an exact variational formula for the limiting pressure of orthogonally invariant Ising spin glasses at every fixed temperature, both almost surely and in expectation. The coupling matrix is a Haar-random rotation of a deterministic spectrum converging to a compactly supported law, with extreme eigenvalues converging to its support edges. The zero-field ground-state energy follows as temperature tends to zero.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

All-temperature pressure for orthogonally invariant Ising spin glasses

OpenAI · September 25, 2026

We determine the limiting pressure of an Ising spin glass with Haar orthogonal eigenvectors, a compact limiting spectral law, and no asymptotic outliers, at every fixed temperature. The pressure converges in expectation and almost surely to a variational formula. We also give the limiting pressure with deterministic external fields whose empirical laws converge in first-moment transport distance, and derive a formula for the zero-field ground-state energy by taking temperature to zero.

Read PDF Download Source

Cite

@misc{OAI:All-temperature-pressure-for-orthogonally-invariant-Ising-spin-glasses-September-25-2026,
  author = {{OpenAI}},
  title = {{All-temperature pressure for orthogonally invariant Ising spin glasses}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/All-temperature-pressure-for-orthogonally-invariant-Ising-spin-glasses-September-25-2026/paper.pdf}{OAI:All-temperature-pressure-for-orthogonally-invariant-Ising-spin-glasses-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

All-temperature pressure for orthogonally invariant Ising spin glasses

Scope

The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional.

The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

Comparator links

Result	Comparator statement
Pressure and ground-state limits for invariant Ising models	InvariantIsing.lean

Scope note on GitHub →