The sum-of-squares framework converts proofs into algorithms so long as those proofs can be formulated as sum-of-squares proofs—proofs that demonstrate their conclusions via the non-negativity of square polynomials. This is a powerful framework that captures many inequalities known in analysis. We formulate sum-of-squares proofs for the trace power method by giving sum-of-squares proofs for non-commutative (matrix) inequalities including the Araki-Lieb-Thirring inequality and Holder's inequality for Schatten norms, and sketch how one might use these proofs to obtain algorithms to constructively find solutions to random optimization problems whose upper bounds can be proven by techniques in random matrix and spin glass theory. Based on work in progress with Juspreet Singh Sandhu.