Oct 6, 2026
Lean formalization in OpenAI math repository (Result 263)
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 'Generalized ionization energies for full Coulomb atoms'. We prove the energy part of the generalized ionization conjecture for full nonrelativistic Coulomb atoms with two electron spin states. The energy needed to remove m electrons is asymptotic to a_{\mathrm{TF}}m^{7/3} whenever m\to\infty and Z/m\to\infty, with the Thomas–Fermi constant in atomic units. We also obtain both conjectured iterated limits.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 263). The Lean development was not rebuilt locally.