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.

翻译：复杂性理论中的民间猜想认为，目前难以触及的针对$\mathbf{NC}^1$或$\mathbf{P}/\operatorname{poly}$的电路下界，是证明如Frege或Extended Frege等系统的强证明复杂性下界的必要步骤。然而，正式建立这种联系本身已是一项艰巨任务，因为正如Pich和Santhanam（2023年）最近观察到的，这将意味着突破性分离$\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$。我们条件性地展示了这种联系，针对的是Krajíček（《符号逻辑杂志》，2004年）引入的隐式扩展弗雷格证明系统（$\mathsf{iEF}$），该系统能够形式化当代复杂性理论的大部分内容。特别地，我们证明：如果$\mathsf{iEF}$能高效地证明标准去随机化假设——即某个具体布尔函数对于亚指数规模电路是平均困难的——那么任何关于$\mathsf{iEF}$证明长度的超多项式下界都意味着$\#\mathbf{P} \not\subseteq \mathbf{FP}/\operatorname{poly}$（进而，例如，意味着$\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$）。我们的证明利用了$\mathsf{iEF}$中对Lund、Fortnow、Karloff和Nisan（《ACM期刊》，1992年）提出的和检查协议可靠性的形式化。这对$\mathsf{iEF}$中电路上界的自证明性具有重要意义。有趣的是，进一步改进我们的结果似乎需要在构建具有更高效证明者的交互式证明系统方面取得进展。