In this talk, I will explain the basics of proof complexity, its connections to NP vs coNP, and SAT solvers lower bounds. One of the frontier proof systems, for which we do not have any lower bounds, is the Res(+) proof system. A recent breakthrough by Efremenko, Garlik, and Itsykson (STOC 2024) established an exponential lower bound for regular Res(+). In our recent work, we proved an exponential lower bound for bounded-depth Res(+).
We will discuss the methods used to prove those lower bounds, such as lifting theorems and Prover-Delayer games.