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