Lean formalization in OpenAI math repository (Result 290)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Bounded recovery for modular spectral averages'. We prove a bounded spectral recovery theorem for a von Neumann algebra with a faithful normal state whose centralizer consists only of scalars. A positive averaged squared norm for an arbitrary bounded Hilbert-space operator on shrinking modular spectral bands can be recovered on uniformly bounded algebra elements with shrinking spectral support. We apply this theorem to spectral intertwining rigidity and obtain an alternative proof of bicentralizer triviality for type III1 factors with separable predual.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 290). The Lean development was not rebuilt locally.