Abstract

For a propositional proof system $\mathcal{P}$ and a polynomial-time function $G: \{0, 1\}^n \to \{0, 1\}^N$ ($N > 10n$), we say that $G$ is a \emph{proof complexity generator} against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the (suitably encoded) statement "$y\not\in\mathrm{Range}(G)$" for every $y \in \{0, 1\}^N$, and $G$ is a \emph{demi-bits generator} against $\mathcal{P}$ if $\mathcal{P}$ cannot efficiently prove the statement "$y \not\in\mathrm{Range}(G)$" for a noticeable fraction of $y \in \{0, 1\}^N$. As can be seen from the definitions, proof complexity generators are qualitatively stronger objects than demi-bits generators.

Our main result is that, perhaps counter-intuitively, every demi-bits generator "contains" exponentially many proof complexity generators. In fact, a random subset of output bits of a demi-bits generator forms a proof complexity generator with constant probability. This result is an extremely simple corollary of Pajor's Lemma (a strengthening of the well-known Sauer--Shelah Lemma). This result also allows us to exhibit the hardness of the Range Avoidance problem ($\text{Avoid}$) in several new, restricted settings of interest.

This is a joint work with Xin Li (JHU) and Yan Zhong (JHU). No prior knowledge about proof complexity is assumed.

Time

2026-08-26  14:00 - 15:00

Speaker

Hanlin Ren is a postdoctoral member at the School of Mathematics, Institute for Advanced Study. Previously, he was a DPhil student at the University of Oxford, advised by Prof. Rahul Santhanam. He is interested in computational complexity theory, and his recent work focuses on circuit complexity, proof complexity, and their metamathematics. Before that, he was an undergraduate student at Tsinghua University and worked on graph algorithms with Prof. Ran Duan.

Room

Room 104