Prove HyperbolicCones (openai/math family 095: Hyperbolicity cones without semidefinite lifts) in Lean 4…
Prove HyperbolicCones (openai/math family 095: Hyperbolicity cones without semidefinite lifts) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 095 of the release, Hyperbolicity cones without semidefinite lifts (Convex and metric…
The task
Context: this statement belongs to family 095 of the release, *Hyperbolicity cones without semidefinite lifts* (Convex and metric geometry). The family as a whole: Disproves the Projected Lax conjecture: some hyperbolicity cones are not spectrahedral shadows. The examples admit no exact finite affine semidefinite…
Part of raising-heart/openai-math.