Lean formalization in OpenAI math repository (Result 228)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A continuum temperature singularity for a radial pair potential'. We construct a stable radial pair potential in three dimensions whose canonical free energy has a strict downward derivative jump at one common finite positive inverse temperature throughout an open interval of positive densities. The potential has a divergent repulsive core, a nontrivial attractive interval, and an integrable tail satisfying \phi(r)=o(r^{-3}). Its free-cube canonical free energy is finite at every positive inverse temperature and density.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 228). The Lean development was not rebuilt locally.