We consider tautologies formed form a pseudo-random number generator, defined in Krajicek [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajicek [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture. This is accompanied by a brief explanation, aimed at non-specialists, of the relation between prepositional proof complexity and bounded arithmetic.