Exploring Propositional Proof Complexity & TFNP at Oberwolfach 2413 🧠

Propositional Proof Complexity and TFNP
Robert Robere, McGill
Oberwolfach workshop 2413 "Proof Complexity and Beyond" (https://www.mfo.de/occasion/2413/www_view)
Monday Mar 25, 2024

A recent line of work [Buss-Johnson '12, Göös et al. '18, Göös et al. '22, Göös et al. '24, Busset al. '22, Davis-Robere '23, Li et al. '24, Hubáček et al. 24] has demonstrated many deep connections between propositional proof systems and total NP search problems (TFNP). The basic correspondence allows us to associate a total search problem $S$ with each propositional proof system $P$ such that the following holds: for every tautology $T$, $T$ has a short proof in $P$ if and only if proving $T$ can be “efficiently reduced” to proving the totality of $S$. This allows us to define a theory of reducibility for proof systems that is analogous to classical reducibility in complexity theory, it has led to the resolution of a number of open problems in both proof complexity and the theory of TFNP, and also has suggested new directions of study in both of these areas.

In this talk we will survey this connection, the recent progress that has been made, and outline some next steps for the development to take.