Tree resolution proofs of the weak pigeon-hole principle

We prove that any optimal tree resolution proof of PHP_n ^m is of size 2^{θ(n log n)}, independently from m, even if it is infinity. So far, only a 2^Ω(n) lower bound has been known in the general case. We also show that any, not necessarily optimal, regular tree resolution proof PHP_n ^m is bounded by 2^{O(n log m)}. To the best of our knowledge, this is the first time the worst case proof complexity has been considered. Finally, we discuss possible connections of our result to Riis´ (1999) complexity gap theorem for tree resolution