We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the first unconditional lower bounds against LEARN-uniform circuits:
-- For all $c\geq 1$, there is $L \in P$ that is not computable by circuits of size $n \cdot (\log n)^c$ generated in deterministic polynomial time with $o(\log n/\log \log n)$ equivalence queries to $L$. In other words, small circuits for $L$ cannot be efficiently learned using a bounded number of EQs.
-- For each $k\geq 1$, there is $L \in NP$ such that circuits for $L$ of size $O(n^k)$ cannot be learned in deterministic polynomial time with access to $n^{o(1)}$ EQs.
-- For each $k\geq 1$, there is a problem in promise-ZPP that is not in FZPP-uniform $SIZE[n^k]$.
-- Conditional and unconditional lower bounds against LEARN-uniform circuits in the general setting that combines randomized uniformity and access to EQs.
In all these lower bounds, the learning algorithm is allowed to run in arbitrary polynomial time, while the hard problem is computed in some fixed polynomial time.
We employ these results to investigate the (un)provability of non-uniform circuit upper bounds (e.g., Is NP contained in $SIZE[n^3]$?) in theories of bounded arithmetic. Some questions of this form have been addressed in recent papers of Krajicek-Oliveira (2017), Muller-Bydzovsky (2020), and Bydzovsky-Krajicek-Oliveira (2020) via a mixture of techniques from proof theory, complexity theory, and model theory. In contrast, by extracting computational information from proofs via a direct translation to LEARN-uniformity, we establish robust unprovability theorems that unify, simplify, and extend nearly all previous results. In addition, our lower bounds against randomized LEARN-uniformity yield unprovability results for theories augmented with the \emph{dual weak pigeonhole principle}, such as $APC^1$ (Jerabek, 2007), which is known to formalize a large fragment of modern complexity theory.
Finally, we make precise potential limitations of theories of bounded arithmetic such as PV (Cook, 1975) and Jerabek's theory $APC^1$, by showing unconditionally that these theories cannot prove statements like ``$NP\not\subseteq BPP \wedge NP\subset io$-P/poly'', i.e., that NP is uniformly ``hard'' but non-uniformly ``easy'' on infinitely many input lengths. In other words, if we live in such a complexity world, then this cannot be established feasibly.
