Speaker: Clemens Hofstadler

Abstract: Algebraic techniques, such as Gröbner bases, have a long and successful history in automatic geometric theorem proving. Recently, these methods have found a new and promising area of application in the context of proving operator statements. Operator statements are first-order formulas involving identities of matrices or, more generally, of linear operators. In this talk, we present how the correctness of an operator statement can be translated into an algebraic statement about noncommutative polynomials, which can be verified automatically using computer algebra. Moreover, we discuss how to certify the invalidity of false operator statements by constructing explicit counterexamples.