Tautologies from pseudo-random generators (Q2736584)

This is the introduction and guide to the author's effort to produce tautologies, hard to be shown to be so, by using random number generators. [The technical side is his ``On the weak pigeonhole principle'', Fundam. Math. 170, No. 1-2, 123-140 (2001; Zbl 0987.03051)]. Here, he starts from the first step: explaining what extended Frege systems are, and why they are used. He gives concise accounts of propositional proof complexity, bounded arithmetic, random generators, and a new hardness condition (called `free'). Also, there are a conjecture, a theorem, relations with pigeonhole principles, and examples and comments. As usual, the author presents a pleasant article: informative, friendly, etc.