We introduce a new and very natural algebraic proof system, which has tight connections to (algebraic) circuit complexity. In particular, we show that any super-polynomial lower bound on any Boolean tautology in our proof system implies that the permanent does not have polynomial-size algebraic circuits ($VNP \neq VP$). As a corollary to the proof, we also show that super-polynomial lower bounds on the number of lines in Polynomial Calculus proofs (as opposed to the usual measure of number of monomials) imply the Permanent versus Determinant Conjecture. Note that, prior to our work, there was no proof system for which lower bounds on an arbitrary tautology implied *any* computational lower bound.
Our proof system helps clarify the relationships between previous algebraic proof systems, and begins to shed light on why proof complexity lower bounds for various proof systems have been so much harder than lower bounds on the corresponding circuit classes. In doing so, we highlight the importance of polynomial identity testing (PIT) for understanding proof complexity.
More specifically, we introduce certain propositional axioms satisfied by any Boolean circuit computing PIT. (The existence of efficient proofs for our PIT axioms appears to be somewhere in between the major conjecture that PIT is in P and the known result that PIT is in P/poly.) We use these PIT axioms to shed light on $AC^0[p]$-Frege lower bounds, which have been open for nearly 30 years, with no satisfactory explanation as to their apparent difficulty. We show that either:
a. Proving super-polynomial lower bounds on $AC^0[p]$-Frege implies $VNP_{\mathbb{F}_p}$ does not have polynomial-size circuits of depth d - a notoriously open question for any $d \geq 4$ - thus explaining the difficulty of lower bounds on $AC^0[p]$-Frege, or
b. $AC^0[p]$-Frege cannot efficiently prove the depth d PIT axioms, and hence we have a lower bound on $AC^0[p]$-Frege.
We also prove many variants on this statement for other proof systems and other computational lower bounds.
Finally, using the algebraic structure of our proof system, we propose a novel way to extend techniques from algebraic circuit complexity to prove lower bounds in proof complexity. Although we have not yet succeeded in proving such lower bounds, this proposal should be contrasted with the difficulty of extending $AC^0[p]$ circuit lower bounds to $AC^0[p]$-Frege lower bounds.
