Oct 6, 2026
Lean formalization in OpenAI math repository (Result 301)
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 trace cone classifies Razak–Jacelon stabilizations'. We prove that the canonical topological cone of all extended lower-semicontinuous tracial weights determines a separable nuclear C∗-algebra after tensoring with the Razak–Jacelon algebra and the compact operators, answering Robert's trace-cone classification question positively. The isomorphism realizes the prescribed cone map, with arbitrary ideal structure and without a density assumption on the finite domains of the weights.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 301). The Lean development was not rebuilt locally.