Formally Verifying Proofs for Algebraic Identities of Matrices.

We consider proof certificates for identities of rectangular matrices. To automate their construction, we introduce an algebraic framework and supply explicit algorithms relying on non-commutative Grobner bases. We address not only verification, but also exploration and reasoning towards establishing new identities and even proving mathematical properties. Especially Grobner-driven elimination theory navigates us to insightful conclusions. We present several applications, that is efficiently formalized proofs for important identities of matrices: cancellation properties of triple products with Moore–Penrose pseudoinverses, a generalized Sherman–Morrison–Woodbury formula and an automated derivation of feedback loops in the famous Youla controller parametrization from control theory.