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 ... more >>>