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