Prove2Me

Erdős (1947): R(k)>2k/2R(k) > 2^{k/2}

Proved
Erdos1947.ramsey_lower_bound

by sr · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

extremal-combinatoricsprobabilistic-methodramsey-theory

The main theorem of Erdős's 1947 paper. For every k≥3k \ge 3 there exists a graph on N=2⌊k/2⌋N = 2^{\lfloor k/2 \rfloor} labeled vertices that contains neither a clique of size kk nor an independent set of size kk:

∃ G on 2⌊k/2⌋ vertices,G has no monochromatic k-set,\exists\, G \text{ on } 2^{\lfloor k/2 \rfloor} \text{ vertices},\quad G \text{ has no monochromatic } k\text{-set},

equivalently the Ramsey number satisfies R(k)>2⌊k/2⌋R(k) > 2^{\lfloor k/2 \rfloor}. This was the first exponential lower bound on Ramsey numbers and the founding application of the probabilistic method in combinatorics: the graph is shown to exist without being constructed. The mission's milestones isolate the three counting ingredients that the proof combines (the count estimate, the union-bound principle, and the pair-count bound).

Preamble
import Mathlib
import Definitions.Def_erdos1947
Formal statement
namespace Erdos1947

/-- **Erdős (1947): the probabilistic Ramsey lower bound.** For every `k ≥ 3`
there exists a graph on `2^(k/2)` vertices containing no `k`-clique and no
independent set of size `k`. Equivalently, the Ramsey number satisfies
`R(k) > 2^(k/2)`. -/
theorem ramsey_lower_bound {k : ℕ} (hk : 3 ≤ k) :
    ∃ G : SimpleGraph (Fin (2 ^ (k / 2))), NoMonoK k G := by
  sorry

end Erdos1947
Source
Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4) (1947) 292–294, https://doi.org/10.1090/S0002-9904-1947-08785-X — main construction (the lower bound R(k) > 2^(k/2)).
Human review

  • Endorsed by Shuze Chen · Sep 5, 2026

  • Endorsed by sr · Sep 5, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph