Speaker
Description
We say that a graph with $n$ vertices is $c$-Ramsey if there is no set of $c \log n$ vertices which form in $G$ either a clique or an independent set. In other words a $c$-Ramsey graph over $n$ nodes is a witness of the fact that $r(c\log n) > n$, where $r(k)$ is the least $N$ such that every graph of size at least $N$ contains a clique or independent set of size $k$.
In searching for hard formulas to prove, proof complexity has often focused on Ramsey principles, by studying upper bounds for $r(k)$, that is on the complexity of certifying that a graph $G$ of size $n$ is $c$-Ramsey.
After reviewing what is known about the complexity of proving Ramsey principles we discuss the case the of $k$-clique Principle, an instantiation of Ramsey principles stating the a graph on $n$ vertices does not contain a $k$-clique. We will present a recent result of ours on the complexity of proving such principle in systems related to the Resolution and when the graph $G$ is a random graph and we discuss why its exact proof complexity in Resolution represents a major open problem.
