We study the *refuter* problems for proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query access to) a purported length-$s$ proof $\pi$ in $P$ that claims to have proved $\varphi$, and our goal is to find an invalid derivation step within $\pi$. As suggested by witnessing theorems in bounded arithmetic, the *computational complexity* of these refuter problems is closely tied to the *metamathematics* of the underlying lower bounds.

We focus on refuter problems corresponding to lower bounds for *resolution*, which is arguably the single most studied system in proof complexity. As a warm-up, we show that many refuter problems for resolution *width* lower bounds are $\mathrm{PLS}$-complete. To capture the complexity of refuter problems for resolution *size* lower bounds, we introduce a new class $\mathrm{rwPHP}(\mathrm{PLS})$ in decision-tree $\mathrm{TFNP}$, which can be seen as a randomized version of $\mathrm{PLS}$.

$\bullet$ We show that the refuter problems for many resolution size lower bounds can be solved in $\mathrm{rwPHP}(\mathrm{PLS})$, including the classic lower bound of Haken [TCS, 1985] for the pigeonhole principle. More generally, we identify a common proof technique that we call "random restriction + width lower bound", and present strong evidence that resolution lower bounds proved by this technique typically have refuter problems in $\mathrm{rwPHP}(\mathrm{PLS})$.
$\bullet$ We then show that the refuter problem for *any* resolution size lower bound is $\mathrm{rwPHP}(\mathrm{PLS})$-hard, thereby demonstrating that the $\mathrm{rwPHP}(\mathrm{PLS})$ upper bound mentioned above is tight. Informally speaking, this means that "$\mathrm{rwPHP}(\mathrm{PLS})$-reasoning" is *necessary* for proving *all* resolution size lower bounds.

Interpreted in bounded arithmetic, our results show that the theory $\mathrm{T}^1_2(\alpha) + \mathrm{dwPHP}(\mathrm{PV}(\alpha))$ characterizes the "reasoning power" required to prove (the "easiest") resolution size lower bounds.

As a corollary, we obtain surprisingly efficient proofs of resolution lower bounds. In particular, we show that many resolution size lower bounds can be proved in low-width *random resolution* [Pudlák--Thapen, CCC'17].

We study the *refuter* problems for proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query access to) a purported length-$s$ proof $\pi$ in $P$ that claims to have proved $\varphi$, and our goal is to find an invalid derivation step within $\pi$. As suggested by witnessing theorems in bounded arithmetic, the *computational complexity* of these refuter problems is closely tied to the *metamathematics* of the underlying lower bounds.

We focus on refuter problems corresponding to lower bounds for *resolution*, which is arguably the single most studied system in proof complexity. As a warm-up, we show that many refuter problems for resolution *width* lower bounds are $\mathsf{PLS}$-complete. To capture the complexity of refuter problems for resolution *size* lower bounds, we introduce a new class $\mathrm{rwPHP}(\mathsf{PLS})$ in decision-tree $\mathsf{TFNP}$, which can be seen as a randomized version of $\mathsf{PLS}$.

$\bullet$ We show that the refuter problems for many resolution size lower bounds can be solved in $\mathrm{rwPHP}(\mathsf{PLS})$, including the classic lower bound of Haken [TCS, 1985] for the pigeonhole principle. More generally, we identify a common proof technique that we call "random restriction + width lower bound", and present strong evidence that resolution lower bounds proved by this technique typically have refuter problems in $\mathrm{rwPHP}(\mathsf{PLS})$.
$\bullet$ We then show that the refuter problem for *any* resolution size lower bound is $\mathrm{rwPHP}(\mathsf{PLS})$-hard, thereby demonstrating that the $\mathrm{rwPHP}(\mathsf{PLS})$ upper bound mentioned above is tight. Informally speaking, this means that "$\mathrm{rwPHP}(\mathsf{PLS})$-reasoning" is *necessary* for proving *all* resolution size lower bounds.

Interpreted in bounded arithmetic, our results show that the theory $\mathsf{T}^1_2(\alpha) + \mathrm{dwPHP}(\mathsf{PV}(\alpha))$ characterizes the "reasoning power" required to prove (the "easiest") resolution size lower bounds.

As a corollary, we obtain surprisingly efficient proofs of resolution lower bounds. In particular, we show that many resolution size lower bounds can be proved in low-width *random resolution* [Pudlák--Thapen, CCC'17].

This paper studies the \emph{refuter} problems, a family of decision-tree $\mathrm{TFNP}$ problems capturing the metamathematical difficulty of proving proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query access to) a purported length-$s$ proof $\pi$ in $P$ that claims to have proved $\varphi$, and our goal is to find an invalid derivation inside $\pi$. As suggested by witnessing theorems in bounded arithmetic, the \emph{computational complexity} of these refuter problems is closely tied to the \emph{metamathematics} of the underlying proof complexity lower bounds.

We focus on refuter problems corresponding to lower bounds for \emph{resolution}, which is arguably the single most studied system in proof complexity. We introduce a new class $\textrm{rwPHP}(\mathrm{PLS})$ in decision-tree $\mathrm{TFNP}$, which can be seen as a randomized version of $\mathrm{PLS}$, and argue that this class effectively captures the metamathematics of proving resolution lower bounds:

\begin{itemize}
\item We show that the refuter problems for many resolution size lower bounds fall within $\textrm{rwPHP}(\mathrm{PLS})$, including the classic lower bound by Haken [TCS, 1985] for the pigeonhole principle. In fact, we identify a common technique for proving resolution lower bounds that we call ``random restriction + width lower bound'', and present strong evidence that resolution lower bounds proved by this technique typically have refuter problems in $\textrm{rwPHP}(\mathrm{PLS})$.

\item We then show that the refuter problem for \emph{any} resolution size lower bound is $\textrm{rwPHP}(\mathrm{PLS})$-hard, thereby demonstrating that the $\textrm{rwPHP}(\mathrm{PLS})$ upper bound mentioned above is tight. It turns out that ``$\textrm{rwPHP}(\mathrm{PLS})$-reasoning'' is \emph{necessary} for proving \emph{any} resolution lower bound \emph{at all}!
\end{itemize}

We view these results as a contribution to the \emph{bounded reverse mathematics} of complexity lower bounds: when interpreted in relativized bounded arithmetic, our results show that the theory $\mathrm{T}^1_2(\alpha) + \textrm{dwPHP}(\mathrm{PV}(\alpha))$ characterizes the ``reasoning power'' required to prove (the ``easiest'') resolution lower bounds. An intriguing corollary of our results is that the combinatorial principle, ``the pigeonhole principle requires exponential-size resolution proofs'', captures the class of $\mathrm{TFNP}$ problems whose totality is provable in $\mathrm{T}^1_2 + \textrm{dwPHP}(\mathrm{PV})$.