The first half of this talk will focus on the following fundamental meta-mathematical question: How difficult is it to prove complexity lower bounds? Inspired by research on this question in bounded arithmetic, we propose to study the "refuter problems" associated with lower bounds, in the context of TFNP and TFZPP. We argue that the *computational complexity* of these refuter problems yield new insights to the *meta-mathematics* of proving lower bounds. We will also discuss some open questions arising from this "TFNP perspective."

In the second half of this talk, we will present our main result, where we conduct a case study on the meta-mathematics of proving lower bounds against resolution, a widely studied proof system. We characterize the complexity of "refuter problems" associated with resolution lower bounds by rwPHP(PLS), a new subclass of TFNP introduced in this work. In particular, we show that "rwPHP(PLS)-reasoning" suffices to prove many resolution lower bounds in the literature, while "rwPHP(PLS)-reasoning" is necessary for proving *any* resolution lower bound *at all*.

Hanlin Ren is a third-year DPhil student at the University of Oxford, advised by Prof. Rahul Santhanam. He is interested in computational complexity theory, and his recent works focused on circuit complexity and pseudorandomness. Prior to that, he was an undergraduate student at Tsinghua University and worked on graph algorithms with Prof. Ran Duan.