Proof complexity is an area of mathematics (and mathematical logic and computational complexity theory in particular) centered around the problem whether the complexity class NP is closed under complementation. With a suitable general definition of a propositional proof system (Cook and Reckhow 1979) this becomes a lengths-of-proofs question: Is there a propositional proof system in which every tautology admits a proof whose length is bounded above by a polynomial in the length of the tautology? The ultimate goal of proof complexity is to show that there is no such proof system; that is, to demonstrate superpolynomial lower bounds for all proof systems.
Strong lower bounds are known for some particular, classical proof systems. (In fact, also surprising upper bounds are known!) The methods used for proving these lower bounds borrow from all parts of logic, from finite combinatorics, from parts of complexity theory including circuit complexity, communication complexity, cryptography, derandomization, from classical algebra like field theory or representation theory, or from abstract concepts of geometry like Euler characteristic and Grothendieck ring.
The purpose of the conference is to bring together researchers in various parts of mathematics and computer science interested in proof complexity. Our ambition is to expose, through invited and contributed lectures, current developments in proof complexity as well as new ideas and directions of research pursued most recently.