Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds

Jiawei Li, Yuhao Li, Hanlin Ren

We study the *refuter* problems for proof complexity lower bounds. Suppose $\ddot{I}†$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corres…