Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
Abstract
We study the *refuter* problems for proof complexity lower bounds. Suppose ϕ 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 π in P that claims to have proved ϕ, and our goal is to find an invalid derivation step within π. As suggested by witnessing theorems in bounded arithmetic, the *computational complexity* of these refuter problems is closely tied to the *metamathematics* of the underlying lower bounds.
Fields of Study & Subjects
Complexity and Algorithms in Graphs
Cryptography and Data Security
Constraint Satisfaction and Optimization
Publication details
- Journal / source
- Proceedings of the 58th Annual ACM Symposium on Theory of Computing
- Publisher
- ACM
- Pages
- 788–798
- Publication date
- 9 June 2026
- Language
- EN