Generalized Lax conjecture: OpenAI counterexample claim; AI-found generic case (Kummer–Netzer)

Your AI and this story

Key facts

• Kummer–Netzer abstract (verbatim): ‘We report a proof found by an artificial intelligence system for the following statement: The hyperbolicity cone of every strictly hyperbolic polynomial is spectrahedral. This establishes the generalized Lax conjecture for the generic case, while the full conjecture remains open.’
• Kummer–Netzer AI declaration (verbatim): ‘The results in this paper were produced almost entirely by an artificial intelligence system. We posed the question and suggested possible approaches. We evaluated the output, clarified and simplified the arguments, checked them for correctness, and edited …’ (the system is not named in the paper)
• OpenAI family 095 summary (CONTENTS.md): ‘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.’ Three manuscripts: ‘A Nonspectrahedral Hyperbolicity Cone’ (24 Sept), ‘An Exact Semidefinite Lift of a Nonspectrahedral Hyperbolicity Cone’ (5 Oct) and ‘Hyperbolicity Cones Without Semidefinite Lifts’ (5 Oct); Lean docs at lean/docs/095.md
• Expert exposition: Kevin Shu, ‘A Digestion of A Counterexample to the Generalized Lax Conjecture’ (Quasicoherent, 12 Oct): ‘The conjecture was disproven in October of 2026 by an internal model from OpenAI, which provided an explicit counterexample to the stated characterization. In a sense, the conjecture being false is the more interesting possibility, as it suggests that there is more richness to the theory of hyperbolic polynomials than previously thought.’
• Background: Helton and Vinnikov proved in 2007 that every real zero polynomial in two variables has a determinantal representation, so every rigidly convex set in the plane is a spectrahedron (Sawall–Schweighofer, §1); the generalized conjecture had also been proved ‘for all hyperbolic cubics in five variables’ (Kummer–Netzer, §1)
• Follow-up: Sawall and Schweighofer (arXiv 2610.37850, 27 Oct) cite both, ‘Kummer and Netzer [KN] used artificial intelligence to generate a proof …’ and OpenAI’s ‘[Ope2] for a hyperbolicity cone that is not a linear projection of a spectrahedral cone’, and build spectrahedral relaxations of rigidly convex sets
• Why it was missed: the Kummer–Netzer abstract names no model, and family 095 was in the release audit without an entry; found on 31 Oct through the Sawall–Schweighofer citation
• Verification status: Kummer–Netzer is an unrefereed preprint checked by its human authors; OpenAI 095 is an unrefereed manuscript with a Lean main statement, accepted by Kevin Shu’s exposition; no refereed version