  We give upper and lower bounds on the power of subsystems of the Ideal Proof
System (IPS), the algebraic proof system recently proposed by Grochow and
Pitassi, where the circuits comprising the proof come from various restricted
algebraic circuit classes. This mimics an established research direction in the
boolean setting for subsystems of Extended Frege proofs, where proof-lines are
circuits from restricted boolean circuit classes. Except one, all of the
subsystems considered in this paper can simulate the well-studied
Nullstellensatz proof system, and prior to this work there were no known lower
bounds when measuring proof size by the algebraic complexity of the polynomials
(except with respect to degree, or to sparsity).
  We give two general methods of converting certain algebraic lower bounds into
proof complexity ones. Our methods require stronger notions of lower bounds,
which lower bound a polynomial as well as an entire family of polynomials it
defines. Our techniques are reminiscent of existing methods for converting
boolean circuit lower bounds into related proof complexity results, such as
feasible interpolation. We obtain the relevant types of lower bounds for a
variety of classes (sparse polynomials, depth-3 powering formulas, read-once
oblivious algebraic branching programs, and multilinear formulas), and infer
the relevant proof complexity results. We complement our lower bounds by giving
short refutations of the previously-studied subset-sum axiom using IPS
subsystems, allowing us to conclude strict separations between some of these
subsystems.
