We prove a quasi-polynomial lower bound on the size of bounded-depth
Frege proofs of the pigeonhole principle PHP^{m}_n where
m= (1+1/{\polylog n})n.
This lower bound qualitatively matches the known quasi-polynomial-size
bounded-depth Frege proofs for these principles.
Our technique, which uses a switching lemma argument like other lower bounds
for ... more >>>