Lean formalization in OpenAI math repository (Result 325)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The complete Crouzeix theorem: optimal similarity and a common positive boundary representation'. We resolve the complete Crouzeix conjecture by proving the sharp constant-two numerical-range inequality for every bounded operator on a complex Hilbert space and every matrix-valued polynomial. No separability assumption is needed. The closure of the numerical range is a complete 2-spectral set, and the bound extends to finite matrix-valued functions holomorphic near that closure. For a finite matrix and a bounded convex domain containing its numerical range with regular real-analytic Jordan boundary, the optimal similarity making its conformal disk image contractive is attained with condition number at most...
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 325). The Lean development was not rebuilt locally.