Lean formalization in OpenAI math repository (Result 291)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Tracial projection methods and uniform property Γ'. For a simple, separable, unital, infinite-dimensional, nuclear, stably finite C∗-algebra with traces, real rank zero of the uniform tracial ultrapower of its uniform tracial completion implies uniform property Γ. This answers Problem XXI of Schafhauser, Tikuisis and White affirmatively. Independently, strict comparison implies Jiang–Su absorption for simple, separable, unital, infinite-dimensional nuclear algebras, resolving the unital Toms–Winter conjecture. Under comparison tested on traces of finite target rank, we also obtain uniform property Γ and absorption for simple, separable, nuclear, stably projectionless algebras whose densely finite traces a...
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 291). The Lean development was not rebuilt locally.