Meta-Mathematics of Algebraic Complexity
We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as Polynomial Calculus Resolution ($\mathsf{PCR}$), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to $\mathsf{NC}^2$, such as $\mathsf{VNC}^2$ and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below $\mathsf{VNC}^2$ into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Under an algebraic analogue of the Krajicek--Razborov conjecture, our results suggest that proving superpolynomial lower bounds for general algebraic circuits will require stronger reasoning than that used in the rank-based proofs studied here. Specifically, we show the following.