Oct 6, 2026
Lean formalization in OpenAI math repository (Result 095)
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 nonspectrahedral hyperbolicity cone'. We construct a homogeneous polynomial of degree 16 in 23 real variables whose hyperbolicity cone has no representation by a finite homogeneous real symmetric linear matrix inequality. This disproves the geometric Generalized Lax conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 095). The Lean development was not rebuilt locally.