The complete Crouzeix conjecture
From OpenAI Aftermath
The complete Crouzeix conjecture asks whether, for every square matrix A and every polynomial P with matrix coefficients, the norm of P[A] is at most twice the maximum of ‖P(z)‖ over the numerical range of A, uniformly in the dimensions and the degree; the scalar case is Crouzeix's 2004 conjecture. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 23 and 26 September 2026, claim the complete conjecture with the sharp constant two, for finite matrices and, through compression, for every bounded operator on a complex Hilbert space. The collection includes a Lean formalization of these statements. 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:
- Crouzeix formulated the constant-two question in 2004 and proved a universal complete bound of 11.08 in 2007; Delyon and Delyon's positive integral representations are a central tool. Crouzeix and Palencia obtained the complete bound 1 + √2, with a final step simplified by Ransford and Schwenninger, and Badea, Crouzeix and Delyon obtained the complete constant two for matrices of order two.
- Recent preprints by Jin, by Lorist and Schwenninger (arXiv:2608.03841) and by Luo give proofs of the scalar constant-two inequality; Lorist and Schwenninger explain why their commutation argument does not immediately extend to matrix coefficients. Åhag, Czyż and Virtanen (arXiv:2608.27346) proved the complete inequality for matrices of order at most three, with arbitrary coefficient size.
The original results
- Claim. Theorem 1.1 of A direct proof of the complete Crouzeix inequality states that for all positive integers n and m, every A in Mn(C) and every polynomial with coefficients in Mm(C), the norm of P[A] is at most twice the maximum of ‖P‖ on the numerical range of A, and that the constant two cannot be decreased. The complete Crouzeix theorem: optimal similarity and a common positive boundary representation proves, for a matrix whose numerical range lies in a bounded convex domain with regular real-analytic Jordan boundary, that the optimal similarity making the conformal image of the matrix contractive is attained with condition number at most two (Theorem 1.1), and that one continuous positive boundary density of mass the identity represents every matrix-valued holomorphic function (Theorem 1.2); its corollaries give the complete inequality for matrices and for bounded operators on arbitrary complex Hilbert spaces, with rational and holomorphic extensions.
- Method, as described: the direct manuscript works from the singular vectors of the polynomial being evaluated and keeps both orders of matrix multiplication; the structural manuscript first chooses an optimal metric and constructs a common positive density valid for every coefficient size. The two manuscripts state that they have separate complete proof paths.
- Sources. The manuscripts The complete Crouzeix theorem and A direct proof of the complete Crouzeix inequality at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the complete inequality with constant two for every matrix and coefficient size, degree and complex coefficients, and that no smaller universal constant works; the same sharp bound for every bounded operator on an arbitrary complex Hilbert space, also for matrix-valued holomorphic and rational functions; and the structural similarity and boundary-density result for regular analytic convex domains, with supporting numerical-range statements. The Comparator statements are
DirectCrouzeix.lean,CompleteCrouzeix.lean,StructuralCrouzeix.lean,CrouzeixHilbert.leanandHilbertCrouzeix.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 "full": the Hilbert-space statement holds for every complete complex inner-product space with no separability assumption and includes an explicit witness for sharpness, and the matrix statements give the universal bound two with its optimality; the numerical-range support statement is supporting only, and the structural statement is an additional finite-dimensional result. It records sandboxed Comparator passes for the five challenges. | 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: CompleteCrouzeix (run 38017370880), DirectCrouzeix (run 38019899278), and CrouzeixHilbert, HilbertCrouzeix and StructuralCrouzeix (run 38051470892) | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept all five solutions. 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) lists none of the five challenges, so all were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-13 | M. Colbrook and contributors, AIM — Open Applied Problems (GitHub), problem 023 | Catalogue | The collection records its problem 023, the complete Crouzeix conjecture for all matrix sizes, coefficient sizes and degrees, as solved by the direct manuscript, noting that the order of the tensor factors differs from its own statement only by a unitary flip. | The status review is described as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". The collection is not affiliated with the American Institute of Mathematics. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscripts; the scalar proofs and the result of Åhag, Czyż and Virtanen precede the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
