theorem RamseyLocalLemma.lovasz_local_lemma_rv_ramsey (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) (h : Real.exp 1 * 2 ^ (1 - ↑(k.choose 2)) * (↑(k.choose 2) * ↑(n.choose (k - 2)) + 1) ≤ 1) : ∃ (G : SimpleGraph (Fin n)), G.CliqueFree k ∧ Gᶜ.CliqueFree k

Application of the random-variable Lovász Local Lemma to the symmetric Ramsey problem: if $e \cdot 2^{1 - \binom{k}{2}} \cdot (\binom{k}{2}\binom{n}{k-2} + 1) \le 1$, there exists a graph on $n$ vertices with no $k$-clique in $G$ or $G^c$.

theorem RamseyLocalLemma.spencer_ramsey_lower_bound (n k : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) (h : Real.exp 1 * 2 ^ (1 - ↑(k.choose 2)) * (↑(k.choose 2) * ↑(n.choose (k - 2)) + 1) < 1) : ∃ (G : SimpleGraph (Fin n)), G.CliqueFree k ∧ Gᶜ.CliqueFree k

Strict-inequality form of Spencer's LLL-based Ramsey lower bound: under $e \cdot 2^{1 - \binom{k}{2}} \cdot (\binom{k}{2}\binom{n}{k-2} + 1) < 1$, there is a graph on $n$ vertices with no $k$-clique in $G$ or $G^c$.