Jan Pich, Kurt Gödel Research Center for Mathematical Logic
Provability of weak circuit lower bounds
Proving lower bounds on the size of Boolean circuits computing explicit Boolean functions is a fundamental problem in the theory of computational complexity. In particular, it presents one of the main approaches to the separation of P and NP, and is closely related to the construction of various learning algorithms. Unfortunately, it is also known as a notoriously hard problem. This triggered the investigation of its proof complexity with a well-known discovery of the natural proofs barrier.
A systematic description of proof complexity of circuit lower bounds can be given in terms of mathematical logic. In this framework, one attempts to show that all existing circuit lower bounds are derivable in a constructive mathematical theory while at the same time no such theory is able to prove strong circuit lower bounds separating P and NP. We will describe the state of the art in this area and focus specifically on giving more constructive proofs of known circuit lower bounds including lower bounds for constant-depth circuits and monotone circuits. These proofs take place inside theories of bounded arithmetic formalizing feasible reasoning or, alternatively, in various extensions of Frege propositional proof system.