The generalized Lax conjecture
The generalized Lax conjecture asserts that every hyperbolicity cone is spectrahedral, that is, the positive-semidefinite region of a finite symmetric linear matrix pencil. The weaker Projected Lax conjecture of Netzer and Sanyal asks whether every hyperbolicity cone is at least a spectrahedral shadow, the linear image of a spectrahedron. Three manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September and 5 October 2026, claim a counterexample to both and an exact semidefinite lift of the first counterexample. The collection includes a Lean formalization of the counterexample to the generalized conjecture. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Lax's question concerned ternary forms. The determinantal theorem of Helton and Vinnikov, with the equivalence explained by Lewis, Parrilo and Ramana, answers it affirmatively in three variables. Brändén constructed a real-zero polynomial no power of which has a definite determinantal representation, while Kummer showed that the related specialized Vámos polynomial still has a spectrahedral cone.
- Positive results cover substantial classes: Brändén proved spectrahedrality for elementary symmetric hyperbolicity cones; Netzer and Sanyal proved that a hyperbolicity cone is a spectrahedral shadow when every nonzero boundary point is a smooth point of its polynomial; Scheiderer obtained second-order-cone lifts for Nash-smooth boundaries. Preprints of September 2026 prove spectrahedrality for hyperbolic cubics in five variables (Netzer) and for strictly hyperbolic polynomials (Kummer and Netzer).
- Scheiderer established nonexistence of semidefinite lifts for general convex semialgebraic sets by local positivity obstructions and asked whether such methods could settle the hyperbolicity-cone question.
- The September manuscript notes that version 1 of a January 2026 preprint by González Nevado states a positive solution of the generalized conjecture (its Theorem 53), and its appendix gives a one-variable example that it says violates the path-containment assertion (Theorem 52) used in that argument.
The original results
- Claim (not spectrahedral). Theorem 1.1 of A nonspectrahedral hyperbolicity cone states that an explicit homogeneous polynomial of degree 20 in 23 real variables, built from the Choi–Lam biquadratic form, is hyperbolic and that its closed hyperbolicity cone is not the positive-semidefinite region of any finite real symmetric linear matrix pencil. Corollary 1.2 obtains a polynomial of degree 16 with the same cone.
- Claim (no semidefinite lift). Theorem 1.1 of Hyperbolicity cones without semidefinite lifts (5 October) states that some hyperbolicity cone has no finite semidefinite lift, with arbitrary real coefficients and any number of auxiliary variables, so that the Projected Lax conjecture and hence the generalized conjecture fail. The manuscript states that the construction is an existence argument in high dimension; its proof tests analytic Gram identities by a finite positive moment functional and uses a finite rank certificate given in an appendix.
- Claim (an exact lift of the first example). An exact semidefinite lift of a nonspectrahedral hyperbolicity cone (5 October) states that the cone of the September counterexample is the projection of a spectrahedron given by a real symmetric pencil of size 100 with 307 auxiliary variables, covering the whole closed cone. The manuscript states that this cone, although it has no semidefinite representation in its original coordinates, admits one when auxiliary variables are allowed.
- Sources (openai/math repository, commit
1581d4c): A nonspectrahedral hyperbolicity cone, Hyperbolicity cones without semidefinite lifts and An exact semidefinite lift of a nonspectrahedral hyperbolicity cone. - Formalization, as described by the repository. The scope note states that the formalized counterexample is an explicit homogeneous polynomial of degree 20 in 23 real variables whose closed hyperbolicity cone is not the positive-semidefinite region of any finite real symmetric linear pencil. It does not mention semidefinite lifts. The Comparator statement is
HyperbolicCones.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker-statement": only the generalized Lax disproof is stated in Lean; the Projected Lax disproof is not, and the companion manuscript shows that the formalized cone has an exact semidefinite lift. It records a sandboxed Comparator pass for HyperbolicCones. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38040214623 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the HyperbolicCones solution (451 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list HyperbolicCones, so the challenge was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_324 (no-lift manuscript) and rank_536 (exact-lift manuscript) in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap in either manuscript. For the no-lift manuscript, the reviewer states that it read all sections and the appendix and reproduced the appendix's rank claims by its own exact computation modulo a prime at a random parameter; its one minor note is that the verification script cited in the appendix is not included in the release folder, which affects reproducibility only. For the exact-lift manuscript, it states that it checked the identities numerically on random instances and the dimension counts, with no minor note. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The positive results and the earlier obstructions are due to the authors named in the Background section, as recounted by the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.