Lower bounds against strong algebraic proof systems, and specifically fragments of the Ideal Proof System (IPS), have been obtained in an ongoing line of work. With the exception of the placeholder model, where the instance itself lacks small circuits, all existing bounds are proved only over large (or characteristic 0) fields, whereas finite fields form the more natural setting for propositional proof complexity. This work establishes lower bounds against fragments of IPS over constant-sized finite fields, resolving an open problem left by a series of prior works beginning with Forbes, Shpilka, Tzameret, and Wigderson (Theor. of Comput.’21), persisting with Behera, Limaye, Ramanathan, and Srinivasan (ICALP’25), and most recently posed by Forbes (CCC’24). We further highlight the importance of the constant-sized finite field regime in IPS by showing that any hard instance in this regime for a sufficiently strong proof system translates into a hard instance against AC0[p]-Frege, whose lower bounds remain a longstanding open problem.

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\displaystyle \sum_{i,j,k,\ell\in[n]}Z_{i_{J}^{\prime}k}\ell x_{i}x_{j}x_{k}x_{\ell}-\beta=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews and Forbes (STOC’22) established recently a constant-depth IPS lower bound, but their hard instance does not have itself small constant-depth circuits, while our instance is computable already with small depth-2 circuits. Our argument relies on extending the recent breakthrough lower bounds against constant-depth algebraic circuits by Limaye, Srinivasan and Tavenas (FOCS’21) to the functional lower bound framework of Forbes, Shpilka, Tzameret and Wigderson (ToC’21), and may be of independent interest. Specifically, we construct a polynomial f computable with small-size constant-depth circuits, such that the multilinear polynomial computing $1/f$ over Boolean values and its appropriate set-multilinear projection are hard for constant-depth circuits.