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

Given two symbolic matrices $X$ and $Y$ of dimensions $m\times n$ and $n\times m$, respectively, the *rank principle* states that when $m = n+1$ and $A$ is a scalar matrix of rank $n+1$, the equation $XY = A$ is unsatisfiable. When $m$ is arbitrarily larger than $n$ and $A$ has ... more >>>