We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHP_n^m where m = (1 + {1 \mathord{\left/ {\vphantom {1 {poly\log n)n}}} \right. \kern-\nulldelimiterspace} {poly\log 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 Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.
Citation:
Josh Buresh-Oppenheim, Paul Beame, Toniann Pitassi, Ran Raz, Ashish Sabharwal, "Bounded-Depth Frege Lower Bounds for Weaker Pigeonhole Principles," focs, pp.583, The 43rd Annual IEEE Symposium on Foundations of Computer Science (FOCS'02), 2002