Proof complexity aims to analyse the power of formal proof systems. Specifically, it is the study of the resources required to certify the truth of mathematical statements. It plays a crucial role in computational complexity and it has close connections to circuit complexity, automated reasoning, and mathematical logic.
A key direction in proof complexity is algebraic proof complexity, which analyses proof systems that use algebraic representations of logical formulas. These systems provide insight into the power and limitations of algebraic methods in proof complexity. Among them, the Ideal Proof System (IPS), introduced by Grochow and Pitassi, is the focus of this talk. IPS represents proofs as algebraic circuits verifying the unsatisfiability of polynomial equations.
In this talk, we will explore the IPS proof system, its connections to algebraic complexity, and recent developments in its study. We will discuss lower bounds for IPS, structural properties of algebraic proofs, and their implications for classical proof complexity questions. Finally, we will highlight open problems and future directions in the field.