This Coq development contains a proof of the finite Ramsey's theorem, which states that for all natural numbers s, t there exists n such that any finite graph of size at least n contains a clique of size s or a completely disconnect subgraph of size t.

Requires CoqHammer >= 1.3.