Horn's eigenvalue conjecture for sums of Hermitian matrices

Let $n$ be a positive integer, and let $S_r^n$ be the recursively defined set of triples of $r$-element subsets of $[n]=\{1,\dots,n\}$. Let $\lambda,\mu,\nu$ be nonincreasing real $n$-tuples. Horn's conjecture. A triple $\lambda,\mu,\nu$ occurs as the eigenvalues of Hermitian $n\times n$ matrices $A,B,C$, respectively, with $C=A+B$, if and only if

$$\sum_{i=1}^n\nu_i=\sum_{i=1}^n\lambda_i+\sum_{i=1}^n\mu_i,$$

and, for every $1\leq r<n$ and every $(I,J,K)\in S_r^n$,

$$\sum_{k\in K}\nu_k\leq\sum_{i\in I}\lambda_i+\sum_{j\in J}\mu_j.$$

This conjecture gives a complete system of inequalities for the classical Hermitian eigenvalue problem and was later proved through the connection with tensor-product multiplicities.