# Hyperbolicity cones without semidefinite lifts

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

- [A nonspectrahedral hyperbolicity cone](../../preprints/A-Nonspectrahedral-Hyperbolicity-Cone-September-24-2026/nonspectrahedral-hyperbolicity-cone.pdf)

## 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](../ComparatorChallenges/HyperbolicCones.lean) |