Abstract:
We prove lower bounds of the form $exp\left(n^{\epsilon_d}\right),$ $\epsilon_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.