Proof complexity as a computational lens lecture 10: Proof of general method for degree lower bounds

Thursday Nov 27, 2025
Proof complexity as a computational lens
Lecture 10: A general method for polynomial calculus degree lower bounds: Proofs
(Jakob Nordström, University of Copenhagen and Lund University)

In this lecture, we give a full proof of correctness for the method developed in [Mikša and Nordström '24] (building on [Alekhnovich and Razborov '03]), which provides a unified way of establishing lower bounds on polynomial calculus degree by building generalized constraint-variable incidence graphs (CVIGs) that are good enough unique-neighbour expanders (a.k.a. boundary expanders). In more technical detail, we show how generalized CVIGs can be used to design pseudo-reduction operators as defined in [Razborov '98]. A degree-D pseudo-reduction operator R for a set of polynomials P behaves like an actual reduction operator modulo the ideal generated by P for all polynomials of degree at most D, and maps all polynomials p derivable in degree at most D to R(p) = 0, but for contradiction in the form of the multiplicative identity 1 of the field it holds that R(1) is non-zero. Therefore, the existence of a degree-D pseudo-reduction operator for a set of polynomials P shows that polynomial calculus cannot derive contradiction from P in degree at most D.

This is lecture 10 on the course "Proof complexity as a computational lens" (https://jakobnordstrom.se/teaching/pr...) given during the winter of 2025/26 at the University of Copenhagen and Lund University.


For more information about MIAO seminars and/or lectures, please visit https://jakobnordstrom.se/miao-seminars/ , or go to https://jakobnordstrom.se/miao-group/ to read more about the MIAO group.

#ProofComplexity