Oct 6, 2026
Lean formalization in OpenAI math repository (Result 296)
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 'Relative generation and the generator problem for finite factors'. We prove that every type II1 factor with separable predual is generated by one operator, equivalently by two self-adjoint operators. Combined with the established direct-integral reduction to this case, this gives an affirmative solution of the generator problem for von Neumann algebras with separable predual.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 296). The Lean development was not rebuilt locally.