OP-00017 Open

The Marcus–de Oliveira determinantal conjecture

Let $A$ and $B$ be normal $n \times n$ complex matrices with eigenvalues $a_1, \dots, a_n$ and $b_1, \dots, b_n$. Does $\det(A + B)$ always lie in the convex hull of the $n!$ points $\prod_{i=1}^{n} (a_i + b_{\sigma(i)})$, $\sigma \in S_n$?

Source: M. Marcus, Indiana Univ. Math. J. 22 (1973); G. N. de Oliveira, Research problem: Normal matrices, Linear Multilinear Algebra 12 (1982), 153–154.

Classification

Primary: RA — Rings and Algebras
Keywords: determinants, normal matrices

References

@article{marcus1973,
  author = {Marcus, Marvin},
  title = {Derivations, {P}l{\"u}cker relations, and the numerical range},
  journal = {Indiana University Mathematics Journal},
  volume = {22},
  pages = {1137--1149},
  year = {1973}
}

@article{deoliveira1982,
  author = {de Oliveira, G. N.},
  title = {Research problem: Normal matrices},
  journal = {Linear and Multilinear Algebra},
  volume = {12},
  pages = {153--154},
  year = {1982}
}

@article{bebianodaprovidencia2025,
  author = {Bebiano, Nat{\'a}lia and da Provid{\^e}ncia, Jo{\~a}o},
  journal = {Mathematics},
  volume = {13},
  pages = {711},
  year = {2025},
  doi = {10.3390/math13050711},
  note = {Survey of the conjecture}
}

@misc{wikipedia,
  title = {Determinantal conjecture},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/Determinantal_conjecture}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/Wikipedia/DeterminantalConjecture.lean#L37},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00017.

/-- OP-00017: The Marcus–de Oliveira determinantal conjecture -/
def Problem_OP_00017 : Prop :=
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (d1 d2 : n → ℂ)
      (U1 U2 : ↥(unitary (Matrix n n ℂ))),
      Matrix.det
          ((↑U1 : Matrix n n ℂ) * Matrix.diagonal d1 * (↑(star U1) : Matrix n n ℂ) +
            (↑U2 : Matrix n n ℂ) * Matrix.diagonal d2 * (↑(star U2) : Matrix n n ℂ)) ∈
        (convexHull ℝ : Set ℂ → Set ℂ)
          {x : ℂ | ∃ (σ : Equiv.Perm n), ∏ i : n, (d1 i + d2 ((σ : n → n) i)) = x}

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00017

theorem resolution : RegistryProblems.Problem_OP_00017 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00017"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00017 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00017, "The Marcus–de Oliveira determinantal conjecture", clopen.solutions.