Proof Complexity (20w5144)
The Banff International Research Station will host the "Proof Complexity" workshop in Banff from January 19 to January 24, 2020. The study of proof complexity was initiated by Cook and Reckhow in 1979 as a way to attack the famous P vs. NP problem (now known as one of the Millennium Prize Problems), and in the ensuing decades many powerful techniques have been discovered for analyzing different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables. During the last 10-15 years the area of proof complexity has seen a revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent breakthroughs give hope that some of these problems might now be within reach. In this workshop, we aim to bring together the whole proof complexity community spanning all of the subareas outlined above. We believe that such a workshop could serve as a powerful stimulus for further progress.
