An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
Jan Krajı́ček, Pavel Pudlák, Alan R. Woods · Random Structures and Algorithms · 1995
Abstract We prove lower bounds of the form exp(nε d), εd > 0, on the length of proofs of an explicit sequence of tautologies, based on the Pigeonhole Principle, in proof systems using formulas of depth d, for any constant d. This is the largest lower bound for the strongest proof system, for which any superpolynomial lower bounds are known.