All open problems
Source labels openChecked July 26, 2026

WikipediaLinear algebra

Determinantal conjecture

Does the determinant of the sum A+BA + B of two n×nn \times n normal complex matrices AA and BB always lie in the convex hull of the n!n! points i(λ(A)i+λ(B)σ(i))\prod_i (\lambda(A)_i + \lambda(B)_{\sigma(i)})? Here the numbers λ(A)i\lambda(A)_i and λ(B)i\lambda(B)_i are the ei...

Mathematical statement

Does the determinant of the sum A+BA + B of two n×nn \times n normal complex matrices AA and BB always lie in the convex hull of the n!n! points i(λ(A)i+λ(B)σ(i))\prod_i (\lambda(A)_i + \lambda(B)_{\sigma(i)})? Here the numbers λ(A)i\lambda(A)_i and λ(B)i\lambda(B)_i are the eigenvalues of AA and BB, and σ\sigma is an element of the symmetric group SnS_n.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

determinantal_conjecture

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem determinantal_conjecture    (n : Type) [Fintype n] [DecidableEq n]    (d1 d2 : n  ℂ) (U1 U2 : unitary (Matrix n n ℂ)) :    (U1 * Matrix.diagonal d1 * star U1 + U2 * Matrix.diagonal d2 * star U2).det       convexHull  { ∏ i, (d1 i + d2 (σ i)) | σ : Equiv.Perm n } := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References