Oct 6, 2026
Lean formalization in OpenAI math repository (Result 293)
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 'Backward intertwiners and a transitive commutant'. We give a negative answer to the hyperinvariant-subspace problem by constructing, on every infinite-dimensional separable complex Hilbert space, a nonzero bounded norm-quasinilpotent operator with no nonzero proper closed hyperinvariant subspace. Its commutant is a proper strongly closed unital transitive complex operator algebra.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 293). The Lean development was not rebuilt locally.