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})$.
