ABSTRACT. 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, 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 Krajíček's 1995 textbook, assumes $n$ only of logarithmic order. It is open whether PV proves known lower bounds in such succinct formalizations. We give such proofs in Jeřábek's theory of approximate counting $APC_1$, an extension of PV 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 Jeřábek'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.