Overview
The area of proof complexity was introduced by Cook and Reckhow in 1979 as a way to tackle the NP vs coNP problem. The overarching goal of the field is to understand how difficult it is to prove certain mathematical facts. Traditionally, the complexity of a theorem is measured as the length of the shortest proof of the theorem in a given formal system. Since the early years of the field many techniques have been developed to analyze concrete proof systems, including establishing relations to other areas of complexity.
In recent years, many exciting results and new connections to proof complexity were discovered or further developed in areas such as, for example, automated proof search, combinatorial optimization, total NP search problems (TFNP), minimum circuit size problem (MCSP), cryptography, learning, approximation algorithms and sumofsquares, extension complexity, algebraic complexity and witnessing theorems. The goal of this workshop is to present some of the classical theory in proof complexity, as well as survey some of the recent exciting connections. The talks will be tutorial in style and we especially encourage attendance from people working in related areas who are not familiar with proof complexity.
The workshop is virtual and will take place over Zoom. FOCS registration is required for all participants. The Zoom link will be made available to registered participants.
Speakers
Sam Buss, Joshua Grochow, Pravesh K. Kothari, Jan Krajíček, Toni Pitassi, Susanna de Rezende, Robert Robere, Rahul Santhanam, Neil Thapen
Program
All times are in Eastern Standard Time (US East Coast/New York time, UTC5).
Videos of all talks are now available here (see also individual links below).
February 7, Morning Session  

12:0012:35  Toni Pitassi  Algebraic Proof Complexity: a gentle introduction  [video] 
12:3513:30  Joshua Grochow  [video]
[slides] 

February 7, Afternoon Session  
17:0017:45  Neil Thapen  A logical approach to TFNP  [video]
[slides] 
17:4518:30  Sam Buss  Total NP Search Problems, Resolution, PLS, and the Wrong Proof Problem  [video]
[slides] 
February 8, Morning Session  
12:0012:45  Robert Robere  Proofs, Circuits, and Communication  [video]
[slides] 
12:4513:30  Jan Krajíček  What do tautologies know about their proofs?  [video]
[slides] 
February 8, Afternoon Session  
17:0017:35  Rahul Santhanam  On the Intractability of Propositional Proof Complexity  [video]
[slides] 
17:3518:10  Pravesh K. Kothari  Refuting random CSPs: eigenvalues to even covers to SDPs, and back  [video]
[slides] 
18:1018:30  Susanna de Rezende  Open Problems  [video]
[slides] 
Abstracts
This session is aimed at introducing researchers in other areas of theory to algebraic (and semialgebraic) proof complexity, and to the wealth of open problems and connections with algebraic circuit complexity, polynomial identity testing, and inapproximability.
Part I: Motivation, history, and introduction to algebraic proof complexity (Toniann Pitassi)
This first talk will give a quick primer on proof complexity, especially as it relates to algebraic proof systems. It will cover some of the history and motivation that led to the study of algebraic proof systems, as well as introduce some wellstudied algebraic proof systems and the relations between them.
Part II: Circuit complexity, ideals and proof systems: connections and recent results (Joshua A. Grochow)
The second talk will cover connections between the Ideal Proof System (IPS), circuit complexity, and more generally complexity in ideals. In particular, it will cover the relation between IPS and VP vs VNP, as well as the recent result of Andrews & Forbes that extends the constantdepth algebraic circuit lower bound of LimayeSrinivasanTavenas to a lower bound on refuting certain polynomial equations in IPS. The talk will highlight the connection between algebraic circuit complexity, algebraic proof complexity, and even Boolean circuit complexity to the complexity not of individual (families of) polynomials, but of arbitrary (families of) polynomials inside an ideal or coset of an ideal.
TFNP search problems have the form: find a witness to an NP property of some object, when a witness is always known to exist. For example, given a hash function from n+1 bits to n bits, find a collision.
Subclasses of TFNP are usually defined by specifying a problem and including all problems reducible to it. It turns out that this is essentially the same as specifying a logical theory and including all problems which the theory proves have a solution. I will talk about what TFNP looks like from this point of view.
Essentially any theory can be used. Some useful ones come from bounded arithmetic, where questions about the provability of some relevant combinatorial principles have been well studied. I will say what the corresponding subclasses of TFNP look like; in particular we get subclasses capturing the strength of some standard models of computation. I will use this approach to study the place of the RAMSEY search problem in TFNP, via a theory that captures reasoning using approximate counting.
This talk discusses Total NP Search (TFNP) problems, including Polynomial Local Search (PLS), polylog width Resolution refutations, connections with Bounded Arithmetic, and the WrongProof Search problem. The last part of the talk discusses similar results for Colored Polynomial Local Search (CPLS), Resolution, and the Res(polylog) refutation system.
The recent discovery and rapid development of querytocommunication lifting theorems has led to the resolution of a number of longstanding open problems in communication, circuit, and proof complexity. These results include the resolution of the AlonSaksSeymour problem, explicit strongly exponential lower bounds on monotone formula complexity, exponential lower bounds on the size of Cutting Planes proofs for random CNF formulas, and many others. One of the key viewpoints enabling the application of these techniques is a deeper understanding of both proof complexity and circuit complexity through the use of certain total search problems. These characterizations greatly expand on several classical results in complexity theory, such as the characterization of circuit depth by KarchmerWigderson games and the equivalence between treelike Resolution and decision trees.
In this talk, we outline a systematic research program that classifies propositional proof systems and circuit classes using the theory of total search problems. The complexity classes in the theory of TFNP, in particular, turn out to provide a natural organizing principle for many proof and circuit classes, and many lower bound results in circuit and proof complexity can be naturally cast into this framework. Future directions and concrete open problems will be discussed.
A recently discovered new proof complexity measure based on algorithmic information seems to play as a fundamental role for proof search as the size measure plays for classical proof complexity centered around lengthsofproofs notions and problems.
One cannot hope to separate unconditionally, for any proof system, the information measure from (the log of) the size measure as that would imply that P differs from NP.
But is it possible to prove nontrivial lower bounds for information in some cases where we failed so far to prove size lower bounds?
This problem seems to be quite inspiring and possibly runs rather deep. I shall explain the necessary background and discuss several facets of the problem.
Superpolynomial proof size lower bounds for strong propositional proof systems such as Frege and EF have remained out of reach, despite intensive efforts. Are there mathematical reasons why strong proof complexity lower bounds are hard to show? I will discuss recent work that sheds light on this question.
Based on joint work with Jan Pich and Iddo Tzameret.
A 3SAT formula with randomly generated m clauses over n variables for m ≫ 5n is unsatisfiable with high probability. For what range of m do such formulas admit short refutations, i.e., efficiently verifiable proofs of unsatisfiability? And when can we find such proofs efficiently?
These questions have a threedecadelong history beginning with the beautiful 1988 paper of Chvátal and Szemerédi. Over time, they have served as a testbed for developing new techniques in proof complexity and averagecase algorithm design in addition to yielding canonical hardness assumptions with applications to cryptography, learning theory, and complexity of statistical inference.
In this talk, I'll present a taste of three techniques developed over the past two decades that yield the strongest results for refuting CSPs: 1) combinatorial techniques based on even covers, 2) spectral methods based on eigenvalues of appropriate matrices, and 3) semidefinite programming/sumofsquares method. My focus will be on recent works that yield significantly simpler arguments that generalize to more general semirandom models of CSPs. In addition, these new analyses reveal a surprising new relationship between combinatorial and spectral/SDPbased techniques and lead to a proof Feige's 2008 conjecture on girthdensity tradeoffs for worstcase hypergraphs.
Based on joint works with Venkatesan Guruswami, Peter Manohar, and Jackson Abascal.
Organizers: Toni Pitassi, Robert Robere, Susanna de Rezende
Workshop cochairs: Alexander Sherstov, Vincent CohenAddad