About:

This workshop brought together researchers working in computational and proof complexity and others working on concrete fundamental hardness questions in complexity theory from diverse perspectives, to explore, discuss and build on recently discovered results in the field. The goal was to support existing directions in the area and at the same time encourage new directions and connections. The non-exhaustive focus of the workshop was existing and new combinatorial, algebraic and probabilistic approaches, and newer logical and meta-mathematical approaches.

Computational complexity theory concerns the mathematical study of the possibilities and limitations of efficient computation. Beyond its intrinsic fundamental nature, understanding which problems are efficiently solvable has many applications in our increasingly computational world: new algorithms are important to make progress in domains such as machine learning and optimization, and new complexity lower bounds (namely, computational impossibility results) are essential for example to provably secure cryptography. Arguably the central question in computational complexity theory is the well-known P vs NP question, which asks if problems whose solutions we can efficiently verify, possess efficient algorithms to find those solutions. Equivalently, the P vs NP question asks if short proofs for mathematical theorems can be found quickly, which is a question about the nature of mathematics itself. Indeed, the centrality of this question to mathematics has been recognized by its choice as one of the seven Millennium Problems by the Clay Mathematical Institute.

Despite significant effort, progress on P and NP and related complexity lower bound problems has been slow. The goal of this workshop was to set up the basis for the emergence of new approaches to these problems as well as the combination of existing approaches in new ways. 

One theme we wished to promote was the interplay between proofs and computation in complexity theory. As an analogy, classical results establish significant links between computability theory, which studies (not necessarily efficient) solvability of computational problems, and proof theory which studies (not necessarily efficient) provability of mathematical theorems. Indeed, simple proofs of the celebrated Gödel's Incompleteness Theorems can be given by using ideas from Turing’s proof of the unsolvability of the Halting Problem. In the resource-bounded setting, where the interest is in efficient computations and proofs, similar (but more intricate) connections are believed to exist, but are relatively under-explored. Recently, there has been exciting work establishing new connections between computational complexity and proof complexity (the latter studies the question of which, predominantly propositional, statements have efficient or short proofs in a given proof system). This includes new forms of feasible interpolation that provides ways to extract computational information from short proofs; new ways to interpret proofs as certain kinds of computational objects, such as algebraic circuits, allowing the transfer of complexity lower bound techniques to lower bounds on proof size and vice versa; new `lifting' results have been found which allow obtaining lower bounds on monotone computation in a generic way from lower bounds on the well-studied Resolution proof system; connections have been found between computational pseudo-randomness and the complexity of proofs in the form of proof complexity generators; and new barriers to efficient provability of strong complexity lower bounds have been found, which can be seen as resource-bounded analogues of the classical theorems of Gödel and Chaitin.

While complexity theory is a truly interdisciplinary field which draws ideas from an increasing number of different mathematical areas, much of the research on complexity lower bounds thus far has focused on combinatorial, algebraic and probabilistic approaches - we believe that bringing in perspectives and techniques from logic can further and deepen our understanding of complexity lower bounds. Indeed, the P vs NP question is inherently meta-mathematical, and so it is reasonable to expect proof complexity-theoretic considerations to be relevant both to the truth value and provability of the P vs NP question. Moreover, we aimed to create new synergies and fresh perspectives by bringing the proof complexity and computational complexity communities together.

Some specific (non-exhaustive) themes we aimed to promote are the following:  (1) Translations between proofs and computations: exploring new forms of proof to-computation conversions, such as generalized feasible interpolation. Also extending and generalising ‘lifting’ approaches, which give equivalences between proof complexity lower bounds and computational complexity lower bounds in different settings;  (2) Algebraic and semi-algebraic proofs and computation: advancing the relations between algebraic computing, algebraic complexity and proof complexity, as well as the study of semi-algebraic proof systems with applications to approximation theory; and  (3) Logic and meta-mathematics of feasible computation: showing new formal barriers on establishing lower bounds on both proofs and computation, by exploiting the inherent meta-mathematical nature of complexity lower bound questions.

Participants: