theorem RamseyLocalLemma.lll_hyp_convert (k n : ℕ) (h : ↑(k.choose 2 * n.choose (k - 2) + 1) * 2 ^ (1 - ↑(k.choose 2)) < 1 / Real.exp 1) : Real.exp 1 * 2 ^ (1 - ↑(k.choose 2)) * (↑(k.choose 2) * ↑(n.choose (k - 2)) + 1) < 1

Algebraic reshuffling: the hypothesis $(\binom{k}{2}\binom{n}{k-2} + 1) \cdot 2^{1 - \binom{k}{2}} < 1/e$ is equivalent to the form $e \cdot 2^{1 - \binom{k}{2}} \cdot (\binom{k}{2}\binom{n}{k-2} + 1) < 1$ required by the LLL.

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

(Theorem 1.1.9, Spencer 1977 — Ramsey lower bound via LLL) If $(\binom{k}{2}\binom{n}{k-2} + 1) \cdot 2^{1 - \binom{k}{2}} < 1/e$, then there exists a graph on $n$ vertices with no $k$-clique in $G$ or $G^c$, witnessing $R(k, k) > n$.