Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$. Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$. It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$.

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$. A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$; here vertices are labeled $0, \dots, N-1$. A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$-set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$. This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$-set is a graph with neither a $k$-clique nor an independent $k$-set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

$$R(k) > 2^{k/2}, \qquad k \ge 3$$

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$-set.

Stronger: the three steps of the proof, as separate targets

1. Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$,

$$\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.$$

2. Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

$$\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.$$

3. Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$-set in $G$ is at most

$$\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.$$

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$.

Difficulty

The central difficulty is that the bad events — "the $k$-set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$-sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$-set ($2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$-set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$-sets of $G$.

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$. The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$, is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic-$k$-set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

• Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$.
• Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
• Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

• Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
• Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
• Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$, for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
• Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$.