Scientific Organisers:

Olaf Beyersdorff, University of Jena

Rahul Santhanam, University of Oxford

Iddo Tzameret, Imperial College London
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 nonexhaustive focus of the workshop was existing and new combinatorial, algebraic and probabilistic approaches, and newer logical and metamathematical 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 wellknown 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 resourcebounded setting, where the interest is in efficient computations and proofs, similar (but more intricate) connections are believed to exist, but are relatively underexplored. 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 wellstudied Resolution proof system; connections have been found between computational pseudorandomness 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 resourcebounded 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 metamathematical, and so it is reasonable to expect proof complexitytheoretic 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 (nonexhaustive) themes we aimed to promote are the following: (1) Translations between proofs and computations: exploring new forms of proof tocomputation 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 semialgebraic proofs and computation: advancing the relations between algebraic computing, algebraic complexity and proof complexity, as well as the study of semialgebraic proof systems with applications to approximation theory; and (3) Logic and metamathematics of feasible computation: showing new formal barriers on establishing lower bounds on both proofs and computation, by exploiting the inherent metamathematical nature of complexity lower bound questions.
Participants:
Programme:
Monday, 4 July 2022  
Registration  
Welcome and introduction  
Proofs, Search & Algorithms  
Susanna F. de Rezende , LTH Lund University  Survey on automatability  
Coffee break  
Mika Goos, EPFL Swisserland  TFNP: Collapses, separations, and characterization  
Oliver Korten, Columbia university, US  Connections between total search and lower bounds  
Lunch break  
Meena Mahajan, The Institute of Mathematical Sciences  Merge Resolution: QBF proofs with inbuilt strategies  
Coffee break  
Christian Ikenmeyer, University of Liverpool  What is in #P and what is not?  
SemiAlgebraic Proofs  
Ilario Bonacina, UPC Universitat Politècnica de Catalunya  On the strength of semialgebraic proof systems  
Welcome reception  
Tuesday, 5 July 2022  
MetaComplexity & MetaMathematics  
Rahul Santhanam, Oxford University  Survey on meta complexity  
Coffee break  
Igor Oliveira, University of Warwick  Unprovability of circuit complexity bounds in bounded arithmetic  
Hanlin Ren, University of Oxford  On the range avoidance problem for circuits  
Jan Pich, University of Oxford  Learning algorithms versus automatability of Frege systems  
Lunch break  
Erfan Khaniki, Institute of Mathematics of the Czech Academy of Sciences  NisanWigderson generators in proof complexity: new lower bounds  
Kilian Risse, KTH Royal Institute of Technology  The minimum circuit size problem is hard for sum of squares  
Coffee break  
Panel discussion  
Wednesday, 6 July 2022  
Combinatorics of Proofs  
Robert Robere, McGill University, Canada  Survey on Lifting  
Coffee break  
Nicola Galesi, Sapienza University Rome  Depth lower bounds in Stabbing Planes  
Neil Thapen, IM CAS  A simple strong tradeoff between height and size in resolution  
Dmitry Sokolov, EPFL Swisserland (ONLINE)  A lower bound for kDNF Resolution on random CNFs  
Lunch  
Free afternoon  
Thursday, 7 July 2022  
Algebra, circuits, and proofs  
Srikanth Srinivasan, Aahrus University, Denmark  Survey on algebraic circuit complexity  
Coffee break  
Anuj Dawar, University of Cambridge  Lower bounds for symmetric arithmetic circuits  
Robert Andrews, University of Illinois at Urbana Champagne  Ideals, determinants, and straightening  
Tuomas Hakoniemi, Imperial College London  Simple hard instances for lowdepth algebraic Proofs  
Lunch break  
Rafael Mendes de Oliveira, University of Waterloo  Succinct semialgebraic representations and computational variants of the generalized Lax conjecture  
Coffee break  
Open problems session  
Dinner at Blonde Restaurant  
Friday, 8 July 2022  
Arnold Beckmann, Swansea University  Survey on bounded arithmetic  
Coffee break  
Pavel Pudlak, Institute of Mathematics, CAS  A hierarchy of propositional proof systems  
Emil Jerabek, Czech Academy of Sciences  Elementary analytic functions in VTC0  
Azza Gaysin, The Charles University in Prague (ONLINE)  Proof complexity of CSP  
Lunch break  
End of workshop. 