Chapter 45, Theorem 2: Ramsey exponential bound

Proved

BookSixth.ramsey_real_bound

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For k at least 2 and every natural N smaller than 2^(k/2) with real exponent, a graph on N vertices has neither a clique nor an independent set of size k. This is the existence formulation of R(k,k)≥2^(k/2); it preserves the real exponent for odd k.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.ramsey_real_bound (k N : ℕ) (hk : 2 ≤ k) (hN : (N : ℝ) < (2 : ℝ)^((k : ℝ)/2)) :
    ∃ G : SimpleGraph (Fin N), NoMono k G := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 45, Theorem 2: Ramsey exponential bound, p. 313. https://doi.org/10.1007/978-3-662-57265-8_45

View graph