Partial Proof of a Conjecture with Implications for Spectral Majorization

TL;DR

This paper advances understanding of a conjecture related to positive definite matrices, demonstrating new matrix families with majorization properties and extending results beyond previous size limits using computational methods.

Contribution

It introduces a new family of matrices with diagonals majorizing their spectrum and extends this property to larger matrices via Kronecker composition, building on prior computational proofs.

Findings

Identified a new matrix family with majorization properties

Extended the property to matrices larger than size 6

Discussed future prospects of AI-assisted proofs

Abstract

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.