Mladen Miksa: On fitting too many pigeons into too few holes

Lunch is served at 12:00 noon (register at http://doodle.com/vwcqud2nwrg5fwbm by Thursday the week before at 8 pm). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

Abstract

If m pigeons want to nest in n separate pigeonholes, they will run into serious problems if m > n. Although this might seem trivial, it is one of the most extensively studied (and fascinating) combinatorial principles in all of proof complexity.

In a breakthrough result, Haken (1985) showed that it is exponentially hard for the resolution proof system to prove that n+1 pigeons don't fit into n holes. However, what happens when the number of pigeons increases? Since it becomes increasingly obvious that not every pigeon can get a different hole, perhaps one can find shorter proofs as the number of pigeons goes to infinity? This notorious open problem was finally resolved by Raz (2001), who established that even for infinitely many pigeons one still needs proofs of exponential length. Raz's result was subsequently simplified and strengthened by Razborov.

In the lunch seminar part of this talk, we will give an overview of Razborov's proof. The presentation will be self-contained and no prerequisites in proof complexity are required. After the break, we will go into technical details and prove the full result.