Proof Complexity of pigeonhole principles

Propositional proof complexity is an area of study that has seen a rapid development over a couple of last decades. It plays as important a role in the theory of feasible proofs as the role played by the complexity of Boolean circuits in the theory of efficient computations.
After a brief review of general underlying definitions, we will concentrate in this talk on lower and upper bounds describing the complexity of particular tautologies that express various forms of the so-called pigeonhole principle. This principle (asserting that there is no injective mapping from $m$ pigeons to $n$ holes when $m>n$) is probably the most extensively studied combinatorial principle in proof complexity. It is amazingly simple and at the same time captures one of the most basic primitives in mathematics and Theoretical Computer Science (counting). Respectively, beginning with the classical paper by Haken (1985), much effort has been put in understanding its proof complexity.
Surprisingly, the complexity of the pigeonhole principle essentially depends on the number of pigeons $m$ (as the function of the number of holes $n$) and on subtle details of its representation as a propositional tautology. This leads to a rich structural picture, and several results obtained during the last couple of years make valuable additions to it.
We will try to summarize what is known about the proof complexity of pigeonhole principles, and what we still would like to prove. If time permits, we will also give some proof details of a new lower bound on the size of resolution proofs of the pigeonhole principle with arbitrarily many pigeons.