When: May 21, 2pm

Where: room G2.91b

**Abstract**

One of the first applications of the probabilistic method in finite combinatorics was Erdos's proof of the existence of graphs on $n$ vertices that do not contain a clique or independent set of size $2\log_2 n$. Since then mathematicians are trying to find an explicit construction of such “Ramsey” graphs. It is, however, possible that no polynomial time construction of Ramsey graphs exists. In this talk we will show a hardness result. We will prove that given any Ramsey graph $G$, any resolution proof showing that $G$ is Ramsey has only superpolynomial proofs.