Erfan Khaniki, University of Oxford

From Proof Complexity to Circuit Complexity via Interactive Protocols

Folklore in complexity theory suspects that circuit lower bounds against NC1 or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation
NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [PS23]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Kra04], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies P^#P ⊈ P/poly. This is a joint work with Noel Arteche, Jan Pich, and Rahul Santhanam.