Lower Bounds against the Ideal Proof System in Finite Fields

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. Specifically, for constant-depth multilinear IPS, we prove that a variant of the knapsack instance studied by Govindasamy, Hakoniemi, and Tzameret (FOCS’22) has no polynomial-size IPS refutation over finite fields when the refutation is multilinear and written as a constant-depth circuit. Our argument has two key ingredients: (i) the recent set-multilinearization result of Forbes, which extends the earlier result of Limaye, Srinivasan, and Tavenas (J. ACM’25) to all fields; and (ii) an extension of the techniques of Govindasamy et al. to finite fields, obtained by constructing a new knapsack variant and generalizing the degree lower bound used in their work. This improves on Behera et al., who obtained related results for fragments of IPS over fields of positive characteristic. Their result requires the field size to grow with the instance, whereas ours does not. Hence, in the constant positive characteristic setting, our IPS lower bound subsumes theirs as it also holds over constant-sized finite fields. Moreover, we separate our proof system from that of Govindasamy et al. by constructing a further knapsack variant and proving a new degree lower bound. We also present new lower bounds for read-once algebraic branching program refutations, roABP-IPS, in finite fields, extending results of Forbes et al. and Hakoniemi, Limaye, and Tzameret (STOC’24). Finally, via an algebraic-to-CNF translation, we show that any lower bound against any proof system at least as strong as (non-multilinear) constant-depth IPS over finite fields for any instance, even a purely algebraic instance (i.e., not a translation of a Boolean formula or CNF), implies a hard CNF formula for the respective IPS fragment, and hence an AC0[p]-Frege lower bound by known simulations over finite fields (Grochow and Pitassi (J. ACM’18)).