Propositional proof complexity aims to prove lower bounds against tautological Boolean formulae for increasingly strong proof systems, with the ultimate goal of separating NP and coNP. A major open problem in this area is lower bounds for AC0[p]-Frege proofs. Since lower bounds for the corresponding circuit class AC0[p] were proved by Razborov and Smolensky through algebraic means, algebraic proof systems such as Nullstellensatz (Beame et. al.) and Polynomial Calculus (Clegg et. al.) were introduced with the intention of better understanding AC0[p]-Frege. Lower bounds for the former systems have been obtained but it has not led to much progress for the latter. In this talk we will show how to obtain lower bounds for a weak version of Polynomial Calculus with extension variables, a proof system which with strong enough extension variables can simulate AC0[p]-Frege. In particular we show that for every prime p and n > 0, there exist tautologies over O(n log n) variables of degree O(log n) such that any Polynomial Calculus proof with o(n^2) extension variables, each depending on O(log n) original variables requires exponential size. This builds on a recent work of Sokolov (STOC 2020) and is joint work with Russell Impagliazzo and Toniann Pitassi, appearing in CCC 2023.
