Pavel Pudlák: The lower bound challenge in proof complexity

In proof complexity we are trying to prove lower bounds on the lengths of proofs for various proof systems. This is similar to what researcher do in circuit complexity, but there are important differences. In circuit complexity (by which I mean the complexity of Boolean circuits) we are essentially stuck: there do not seem to be easily accessible problems, and we have some negative results that explain why---the impossibility of the so called natural proofs. In contrast, in proof complexity there seems to be more problems about lower bounds that should be solvable with the currently available of methods, or their extensions. Furthermore, proof complexity introduces new kinds of computing structures for Boolean functions, thus providing us with new problems in Boolean function complexity theory. In the lecture I will focus on the method of feasible interpolation as a viable approach to proving lower bounds for stronger proof systems.