Lean formalization in OpenAI math repository (Result 227)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Critical slowing down in the Sherrington–Kirkpatrick model'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 227). The Lean development was not rebuilt locally.