This is a seminar work and presentation on the main result in Razborov's 1998 paper.
A major endavour of theoretical computer science is investigating relationships between complexity classes. Maybe the most well known of these is the question of P = NP. Of particular interest to logicians is the related question of NP = coNP since it is the case if and only if every proof system of propositional formulae has some family of unsatisfiable formulae that require a super-polynomially long proof to be proven unsatisfiable.
In this seminar we will look at the only known lower bound for the polynomial calculus proof system. The set of formulae we use are ones encoding the pigeonhole principle, the idea that if you have more pigeons than pigeon holes, at least two of them need to share a hole. The core of the proof watches the pigeons perform a dance, before we unfortunately have to take a dark turn and kill some of them.