Hard generator conjecture for propositional proof systems

A generator is a map $g:{0,1}^*\rightarrow{0,1}^*$ whose restriction to inputs of length $n$ maps into strings of length $m(n)>n$ and is computed by circuits of size polynomial in $m(n)$. For a propositional proof system $P$, let ${\bf s}_P(\varphi)$ denote the minimum length of a $P$-proof of the tautology $\varphi$. A generator is hard for $P$ if, for every $c\geq 1$,

$$\bf s_P(\tau(g)_b)\leq |\tau(g)_b|^c\leq |b|^{O(c)}$$

holds for only finitely many $b$, where $\tau(g)_b$ expresses that $b$ is not in the range of the circuit defining $g$. Hard generator conjecture. There exists a generator hard for all propositional proof systems; equivalently, its range intersects every infinite nondeterministic polynomial-time set. In fact, such a generator exists that is computable in polynomial time. This hypothesis is used in proof complexity to obtain generators whose range avoids efficiently recognizable hard sets, and its relationship with proof-system simulations is a central theme of the paper.