  In this paper we report on new results relating to a conjecture regarding
properties of $n\times n$, $n\leq 6$, positive definite matrices. The
conjecture has been proven for $n\leq 4$ using computer-assisted sum of squares
(SoS) methods for proving polynomial nonnegativity. Based on these proven
cases, we report on the recent identification of a new family of matrices with
the property that their diagonals majorize their spectrum. We then present new
results showing that this family can extended via Kronecker composition to
$n>6$ while retaining the special majorization property. We conclude with
general considerations on the future of computer-assisted and AI-based proofs.
