A map $g:\{0,1\}^n \to \{0,1\}^m$ ($m > n$) is a hard proof complexity generator for a proof system P if and only if for every string $b \in \{0,1\}^m\setminus Range(g)$, the formula $\tau_b(g)$ naturally expressing $b \notin Range(g)$ requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov [Annals of Mathematics 2015] conjectured that if $A$ is a suitable matrix and $f$ is an NP $\cap$ Co-NP function hard-on-average for P/poly, then NW$_{\{f,A\}}$ is a hard proof complexity generator for Extended Frege. In this talk, we prove a form of Razborov's conjecture for AC$^\circ$-Frege. We show that for any symmetric NP $\cap$ Co-NP function $f$ that is exponentially hard for depth two AC$^\circ$ circuits, NW$_{\{f,A\}}$ is a hard proof complexity generator for AC$^\circ$-Frege in a natural setting.

Zoom room information:
https://us06web.zoom.us/j/81916335336?pwd=5zQT4lutMiBoY5Xp1pkFGtbqiaGozg.1
Meeting ID: 819 1633 5336
Passcode: 559618
Venue: Niavaran, Lecture Hall 1