Oct 6, 2026
Lean formalization in OpenAI math repository (Result 215)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Exponential decay in two-dimensional classical O(n) models'. We prove exponential decay of two-point correlations for the classical nearest-neighbor O(n) model on the square lattice, for every n ≥ 3 and every finite positive inverse temperature. The estimate is uniform over finite free-boundary subgraphs and bounded nonnegative edge strengths. This resolves positively the all-temperature exponential spin-decay conjecture for these models.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 215). The Lean development was not rebuilt locally.