  Folklore in complexity theory suspects that circuit lower bounds against
$\mathbf{NC}^1$ or $\mathbf{P}/\operatorname{poly}$, currently out of reach,
are a necessary step towards proving strong proof complexity lower bounds for
systems like Frege or Extended Frege. Establishing such a connection formally,
however, is already daunting, as it would imply the breakthrough separation
$\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$, as recently
observed by Pich and Santhanam (2023).
  We show such a connection conditionally for the Implicit Extended Frege proof
system ($\mathsf{iEF}$) introduced by Kraj\'i\v{c}ek (The Journal of Symbolic
Logic, 2004), capable of formalizing most of contemporary complexity theory. In
particular, we show that if $\mathsf{iEF}$ proves efficiently the standard
derandomization assumption that a concrete Boolean function is hard on average
for subexponential-size circuits, then any superpolynomial lower bound on the
length of $\mathsf{iEF}$ proofs implies $\#\mathbf{P} \not\subseteq
\mathbf{FP}/\operatorname{poly}$ (which would in turn imply, for example,
$\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$). Our proof
exploits the formalization inside $\mathsf{iEF}$ of the soundness of the
sum-check protocol of Lund, Fortnow, Karloff, and Nisan (Journal of the ACM,
1992). This has consequences for the self-provability of circuit upper bounds
in $\mathsf{iEF}$. Interestingly, further improving our result seems to require
progress in constructing interactive proof systems with more efficient provers.
