Prove HilbertCrouzeix (openai/math family 325: The complete Crouzeix conjecture) in Lean 4 with Mathlib…
Prove HilbertCrouzeix (openai/math family 325: The complete Crouzeix conjecture) in Lean 4 with Mathlib…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 325 of the release, The complete Crouzeix conjecture (Functional analysis). The family…
The task
Context: this statement belongs to family 325 of the release, *The complete Crouzeix conjecture* (Functional analysis). The family as a whole: Resolves the complete Crouzeix conjecture: for every bounded operator $A$ on a complex Hilbert space and every finite matrix-valued polynomial $P$, one has $\lVert…
Part of raising-heart/openai-math.