Hyperbolicity cones without semidefinite lifts

3 papersLean

Disproves the Projected Lax conjecture: some hyperbolicity cones are not spectrahedral shadows. The examples admit no exact finite affine semidefinite lift, regardless of the number of auxiliary variables or the real coefficients used. This also disproves the generalized Lax conjecture that every hyperbolicity cone is spectrahedral.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Hyperbolicity Cones Without Semidefinite Lifts

OpenAI · October 5, 2026

We prove that not every hyperbolicity cone is a spectrahedral shadow: some closed hyperbolicity cones admit no finite affine semidefinite lift, even with arbitrary real coefficients and any finite number of auxiliary variables. This disproves the Projected Lax Conjecture and hence the generalized Lax conjecture.

Read PDF Download Source

Cite

@misc{OAI:Hyperbolicity-Cones-Without-Semidefinite-Lifts-October-5-2026,
  author = {{OpenAI}},
  title = {{Hyperbolicity Cones Without Semidefinite Lifts}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Hyperbolicity-Cones-Without-Semidefinite-Lifts-October-5-2026/nonliftable-hyperbolicity.pdf}{OAI:Hyperbolicity-Cones-Without-Semidefinite-Lifts-October-5-2026}},
  year = {2026}
}

A nonspectrahedral hyperbolicity cone

OpenAI · September 24, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:A-Nonspectrahedral-Hyperbolicity-Cone-September-24-2026,
  author = {{OpenAI}},
  title = {{A nonspectrahedral hyperbolicity cone}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Nonspectrahedral-Hyperbolicity-Cone-September-24-2026/nonspectrahedral-hyperbolicity-cone.pdf}{OAI:A-Nonspectrahedral-Hyperbolicity-Cone-September-24-2026}},
  year = {2026}
}

An Exact Semidefinite Lift of a Nonspectrahedral Hyperbolicity Cone

OpenAI · October 5, 2026

We construct an exact semidefinite lift of the explicit nonspectrahedral hyperbolicity cone in twenty-three variables defined in the companion paper. The lift is a homogeneous real symmetric pencil of size 100 with 307 auxiliary variables and represents the entire closed cone, including every point with singular X. Thus, although this cone has no semidefinite representation in its original coordinates, it admits one when auxiliary variables are allowed. The stated sizes are not claimed to be minimal.

Read PDF Download Source

Cite

@misc{OAI:An-Exact-Semidefinite-Lift-of-a-Nonspectrahedral-Hyperbolicity-Cone-October-5-2026,
  author = {{OpenAI}},
  title = {{An Exact Semidefinite Lift of a Nonspectrahedral Hyperbolicity Cone}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-Exact-Semidefinite-Lift-of-a-Nonspectrahedral-Hyperbolicity-Cone-October-5-2026/Exact-Semidefinite-Lift-of-a-Nonspectrahedral-Hyperbolicity-Cone.pdf}{OAI:An-Exact-Semidefinite-Lift-of-a-Nonspectrahedral-Hyperbolicity-Cone-October-5-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A nonspectrahedral hyperbolicity cone

Scope

The generalized Lax conjecture predicts that every hyperbolicity cone is spectrahedral. The formalized counterexample is an explicit homogeneous polynomial of degree \(20\) in \(23\) real variables. It is hyperbolic, but its closed hyperbolicity cone cannot be represented as the positive-semidefinite region of any finite real symmetric linear matrix pencil, in any positive matrix size.

Comparator links

Result	Comparator statement
Nonspectrahedral hyperbolicity cone	HyperbolicCones.lean

Scope note on GitHub →