We consider the resolution proof complexity of propositional formulas which encode random instances of graph $k$-colorability. We obtain a tradeoff between the graph density and the resolution proof complexity.
For random graphs with linearly many edges we obtain linear-exponential lower bounds on the length of resolution refutations. For any $\epsilon>0$, we obtain sub-exponential lower bounds of the form $2^{n^\delta}$ for some $\delta>0$ for non-$k$-colorability proofs of graphs with $n$ vertices and $O(n^{\frac{3}{2}-\frac{1}{k}-\epsilon}$ edges. We obtain sharper lower bounds for Davis-Putnam-DPLL proofs and for proofs in a system considered by McDiarmid.

We also show that very simple algorithms achieve qualitatively similar running times.