We consider tautologies formed from a pseudo-random
number generator, defined in Kraj\'{\i}\v{c}ek \cite{Kra99}
and in Alekhnovich et.al. \cite{ABRW}.
We explain a strategy of proving their hardness for EF via
a conjecture about bounded arithmetic formulated
in Kraj\'{\i}\v{c}ek \cite{Kra99}. Further we give a
purely finitary statement, in a form of a hardness condition
posed on a function, equivalent to the conjecture.
This is accompanied by a brief explanation, aimed at
non-logicians, of the relation between propositional
proof complexity and bounded arithmetic.