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 AC^0, for AC^0[p] (for some n of intermediate order), and for monotone circuits. 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.