Oct 6, 2026
Lean formalization in OpenAI math repository (Result 228)
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 'A radial continuum phase transition with algebraic decay'. We construct a bounded, continuous, stable radial pair potential in three dimensions with |\phi(r)|\le Cr^{-3-1/32} for r ≥ 1. Throughout an open interval of positive densities, its canonical thermodynamic free energy is finite at every positive inverse temperature and has a strict downward derivative jump at one common finite positive inverse temperature.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 228). The Lean development was not rebuilt locally.