We give a new approach to the fundamental question of whether proof complexity lower bounds for concrete propositional proof systems imply super-polynomial Boolean circuit lower bounds.

For any poly-time computable function $f$, we define the witnessing formulas $w_n^k(f)$, which are propositional formulas stating that for any circuit $C$ of size $n^k$ on $n$ variables and for any formula $\phi$ of size $n$, either $C$ computes a satisfying assignment to $\phi$ or $f$ verifiably refutes that $C$ computes SAT on instances of length $n$. We show that if the witnessing formulas are tautologies, then any super-polynomial lower bound for Extended Frege augmented with $w_n^k(f)$ axioms implies that SAT requires super-polynomial size Boolean circuits. We also give an unconditional equivalence between proof complexity lower bounds for a concretely defined strong (non-uniform) propositional proof system and super-polynomial circuit lower bounds for the Discrete Logarithm problem.

We give consequences for the meta-mathematics of several major questions in computational complexity, including whether one-way functions can be based on the worst-case hardness of NP, whether there is a dichotomy between one-way functions and worst-case learning with membership queries over the uniform distribution, and whether there are feasibly constructible anti-checkers for Satisfiability. We show that for each of these questions, provability of a positive answer in any system of bounded arithmetic would imply new connections between propositional proof complexity and circuit complexity.

Our results rely on a new notion of ``self-provability" of upper bounds, which might be independently interesting.