Cook and Reckhow 1979 pointed out that NP is not closed under complementation iff there is no propositional proof system that admits polynomial size proofs of all tautologies. Theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus at a conjecture from K.2004 in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows: * There exist a p-time function $g$ stretching each input by one bit such that its range intersects all infinite NP sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from K.2009 is a good candidate for $g$. We define a new hardness property of generators, the $\bigvee$-hardness, and shows that one specific gadget generator is the $\bigvee$-hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite NP sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite NP sets.

翻译：Cook和Reckhow（1979）指出，NP不在补运算下封闭当且仅当不存在一个命题证明系统能够对所有重言式提供多项式大小的证明。证明复杂度生成元理论旨在构造对强证明系统乃至所有证明系统困难的重言式集合。我们聚焦于K.2004中提出的关于该理论基础的猜想：存在一个对所有证明系统都困难的证明复杂度生成元。该猜想可等价地表述为（针对p时间生成元）而不涉及证明复杂度概念：*存在一个将每个输入拉伸一位的p时间函数$g$，使得其值域与所有无限NP集合相交。我们从多个维度考察该猜想，包括其与有界算术（见证性和独立性结果）、时间有界Kolmogorov复杂度、命题证明系统的可行析取性质以及证明搜索复杂度的联系。我们认为K.2009提出的特定工具生成元是$g$的优良候选。我们定义了生成元的新困难性质——$\bigvee$-困难性，并证明一个特定的工具生成元是$\bigvee$-最困难的（对于任意足够强的证明系统）。我们定义了可行无限NP集合类，并证明，在电路复杂性假设下，该猜想对所有可行无限NP集合成立。