We study the diagonalization in the context of proof
complexity. We prove that at least one of the
following three conjectures is true:

1. There is a boolean function computable in E
that has circuit complexity $2^{\Omega(n)}$.

2. NP is not closed under the complement.

3. There is no p-optimal propositional proof system.

We note that a variant of the statement seems to have
a bearing on the existence of good proof complexity generators.
In particular, we prove that if a minor variant
of a recent conjecture of Razborov is true (stating conditional
lower bounds for the Extended Frege proof system EF) then
actually unconditional lower bounds would follow for EF.