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 P V 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 P V 1 proves known lower bounds in such succinct formalizations. We give such proofs in Jerabek’s theory of approximate counting AP C 1 , an extension of P V 1 formalizing probabilistic polynomial time reasoning. Specifically, we prove in AP C 1 lower bounds for the parity function and A C 0 , for the mo d q counting function and A C 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 AP C 1 formalizations can be applied to derive a conditional upper bound on succinct propositional formulas obtained by witnessing extracted from the AP C 1 proofs. Namely, we show these formulas have short Extended Frege E F 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 A C 0 [ p ] quasipolynomial size lower bounds; these proofs are in Jerabek’s proof system W F . 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.