Oct 6, 2026
Lean formalization in OpenAI math repository (Result 299)
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 'The Kirchberg–Rørdam character criterion'. We prove the Kirchberg–Rørdam character criterion: for every free ultrafilter on ℕ, a nonzero unital separable complex C∗-algebra absorbs the Jiang–Su algebra if and only if its norm central-sequence algebra has no characters. We also prove that the infinite minimal tensor power of every nonzero unital separable complex C∗-algebra without characters is \mathcal Z-stable and contains a unital copy of \mathcal Z.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 299). The Lean development was not rebuilt locally.