The Proof Complexity of Polynomial Identities

Devising an efficient deterministic - or even a non-deterministic sub-exponential time - algorithm for testing polynomial identities is a fundamental problem in algebraic complexity and complexity at large. Motivated by this problem, as well as by results from proof complexity, we investigate the complexity of proving polynomial identities. To this end, we study a class of equational proof systems, of varying strength, operating with polynomial identities written as arithmetic formulas over a given ring. A proof in these systems establishes that two arithmetic formulas compute the same polynomial, and consists of a sequence of equations between polynomials, written as arithmetic formulas, where each equation in the sequence is derived from previous equations by means of the polynomial-ring axioms. We establish the first non-trivial upper and lower bounds on the size of equational proofs of polynomial identities, as follows: 1. Polynomial-size upper bounds on equational proofs of identities involving symmetric polynomials and interpolation-based identities. In particular, we show that basic properties of the elementary symmetric polynomials are efficiently provable already in equational proofs operating with depth-4 formulas, over infinite fields. This also yields polynomial-size depth-4 proofs of the Newton identities, providing a positive answer to a question posed by Grigoriev and Hirsch. 2. Exponential-size lower bounds on (full, unrestricted) equational proofs of identities over certain specific rings. 3. Exponential-size lower bounds on analytic proofs operating with depth-3 formulas, under a certain regularity condition. The "analytic" requirement is, roughly, a condition that forbids introducing arbitrary formulas in a proof and the regularity condition is an additional structural restriction. 4. Exponential-size lower bounds on one-way proofs (of unrestricted depth) over infinite fields. Here, one-way proofs are analytic proofs, in which one is also not allowed to introduce arbitrary constants. Furthermore, we determine basic structural characterizations of equational proofs, and consider relations with polynomial identity testing procedures. Specifically, we show that equational proofs efficiently simulate the polynomial identity testing algorithm provided by Dvir and Shpilka.