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 bounded-depth ...
more >>>