Algebraic Proof Systems: An Algebraic Approach to Analysing Proofs

Abstract

Proof complexity studies the power of formal proof systems. More specifically, it investigates the resources required to certify the truth of mathematical statements. The area plays a central role in computational complexity and has close connections to circuit complexity, automated reasoning, and mathematical logic.

A key direction within the field is algebraic proof complexity, which studies proof systems based on algebraic representations of logical formulas. These systems provide insight into the power and limitations of algebraic methods for reasoning. Among them, the Ideal Proof System (IPS), introduced by Grochow and Pitassi, is the focus of this talk. IPS represents proofs as algebraic circuits certifying the unsatisfiability of systems of polynomial equations.

In this talk, we will explore the IPS proof system, its connections to algebraic complexity, and recent developments in the area. We will discuss lower bounds for IPS, structural properties of algebraic proofs, and their implications for classical questions in proof complexity. We will also discuss recent developments involving symmetry and lifting, barriers to current lower-bound techniques, and recent progress toward proving lower bounds for CNF instances. Finally, we will highlight several open problems and directions for future research.