Oct 6, 2026
Lean formalization in OpenAI math repository (Result 325)
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 'A direct proof of the complete Crouzeix inequality'. We give a direct proof of the sharp constant-two numerical-range inequality for matrix-valued polynomials in all finite base and coefficient dimensions. This resolves the complete Crouzeix conjecture in its matrix formulation, including matrices whose numerical ranges are points or line segments.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 325). The Lean development was not rebuilt locally.