We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length $n$. In 1995 Razborov showed that many can be proved in $PV_1$, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small $n$ of doubly logarithmic order. It is open whether $PV_1$ proves known lower bounds in such succinct formalizations for $n$ of logarithmic order. We give such proofs in Jerabek’s theory of approximate counting $APC_1$, an extension of $PV_1$ formalizing probabilistic polynomial time reasoning: for parity and $AC^0$, for $mod_q$ and $AC^0[p]$ (only for $n$ slightly smaller than logarithmic), and for $k$-clique and monotone circuits. We also formalize Razborov and Rudich’s natural proof barrier.

We ask for short propositional proofs of circuit lower bounds expressed succinctly by propositional formulas of size $n^{O(1)}$ or at least much smaller than the $2^{O(n)}$ size of the common ``truth table" formula. We discuss two such expressions: one via feasible functions witnessing errors of circuits, and one via the anticheckers of Lipton and Young 1994. Our $APC_1$ formalizations yield conditional upper bounds for the succinct formulas obtained by witnessing: we get short Extended Frege proofs from general circuit lower bounds expressed by the common “truth-table” formulas. We also show how to construct in quasipolynomial time propositional proofs of quasipolynomial size tautologies expressing $AC^0[p]$ quasipolynomial size lower bounds; these proofs are in Jerabek’s proof system $WF$.

We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length $n$. In 1995 Razborov showed that many can be proved in Cook’s theory $PV_1$, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small $n$ of doubly logarithmic order. A more common formalization, considered in Krajicek’s 1995 textbook, assumes $n$ only of logarithmic order. It is open whether $PV_1$ proves known lower bounds in such succinct formalizations. We give such proofs in Jerabek’s theory of approximate counting $APC_1$, an extension of $PV_1$ formalizing probabilistic polynomial time reasoning. Specifically, we prove in $APC_1$ lower bounds for the parity function and $AC^0$, for the $mod_q$ counting function and $AC^0[p]$ (for some $n$ of intermediate order), and for the $k$-clique function and monotone circuits. We also formalize Razborov and Rudich’s natural proof barrier.

Further, we ask for feasibly constructible propositional proofs of circuit lower bounds. We discuss two ways to succinctly express circuit lower bounds by propositional formulas of polynomial size $n^{O(1)}$ or at least much smaller than size $2^{O(n)}$ of the common formula based on the truth table of the function: one via feasible functions witnessing errors of circuits trying to compute some hard function, and one via the anticheckers of Lipton and Young 1994 or partial truth tables. Our $APC_1$ formalizations can be applied to derive a conditional upper bound on succinct propositional formulas obtained by witnessing extracted from the $APC_1$ proofs. Namely, we show these formulas have short Extended Frege $EF$ proofs from general circuit lower bounds expressed by the common “truth-table” formulas. We also show how to construct in quasipolynomial time propositional proofs of quasipolynomial size tautologies expressing $AC^0[p]$ quasipolynomial size lower bounds; these proofs are in Jerabek’s proof system $WF$. The last result is proved by formalizing a variant of Razborov’s and Rudich’s naturalization of Smolensky’s proof for partial functions on the propositional level.