Algebraic Proof Systems (Invited Talk)

Abstract

Given a set of polynomial equations over a field F, how hard is it to prove that they are simultaneously unsolvable? In the last twenty years, algebraic proof systems for refuting such systems of equations have been extensively studied, revealing close connections to both upper bounds (connections between short refutations and efficient approximation algorithms) and lower bounds (connections to fundamental questions in circuit complexity.)
The Ideal Proof System (IPS) is a simple yet powerful algebraic proof system, with very close connections to circuit lower bounds: [Joshua A. Grochow and Toniann Pitassi, 2018] proved that lower bounds for IPS imply VNP ≠ VP, and very recently connections in the other direction have been made, showing that circuit lower bounds imply IPS lower bounds [Rahul Santhanam and Iddo Tzameret, 2021; Yaroslav Alekseev et al., 2020].
In this talk I will survey the landscape of algebraic proof systems, focusing on their connections to complexity theory, derandomization, and standard proposional proof complexity. I will discuss the state-of-the-art lower bounds, as well as the relationship between algebraic systems and textbook style propositional proof systems. Finally we end with open problems, and some recent progress towards proving superpolynomial lower bounds for bounded-depth Frege systems with modular gates (a major open problem in propositional proof complexity).