This is a very nicely written paper. The subject matter is the length of a proof of the pigeonhole principle in propositional calculus. This principle, \(\text{PHP}_n\) (\(n+1\) pigeons in \(n\) holes), is formulated by using propositional variables \(p_{ij}\) (pigeon \(i\) is in hole \(j\)). A Frege system is any propositional calculus with a finite number of axiom schemes and of inference rules (i.e. a system usually used). It was expected that a proof of \(\text{PHP}_n\) is longer than any bound given by a polynomial in \(n\). But S. Buss presented a polynomial size proof [J. Symb. Logic 52, 916-927 (1987; Zbl 0636.03053)]. In this paper, the authors prove the non-existence of a polynomial bound if the depth of the formulas in the proof is required to be limited (depth = the number of changes of connectives). Indeed, the size of a proof is at least \(\exp (n^{(5+ o(1) )^{-d}})\), where \(d\) is the given bound of depth. Besides this new result and the intricate proof using probabilistic combinatorial lemmas, the paper has the merit of being a clear and pleasant presentation. The authors first state an obvious, naïve approach for proving the result, then where it breaks down, and so how to be modified; new notions are introduced with good explanation, and so forth. Here is a prominent example: “Unfortunately it is not true in general that \(|S|\leq 2s\) and we have to employ random map \(\rho\) from \(R_p\) to achieve this.” [p. 29, ll. 4&5].