Graph Ramsey numbers

DefinitionThe Ramsey property for cliques#✓fully proved

For natural numbers \(s\), \(t\) and \(N\), the classical Ramsey property for \((s, t)\) holds at \(N\) when every simple graph \(G\) on \(N\) vertices contains the complete graph \(K_s\) as a subgraph, or its complement \(\overline{G}\) contains \(K_t\) as a subgraph.

Thus the graph and its complement encode the two colors of a complete graph.

def classicalRamsey (s t N : ℕ) : Prop :=
  ∀ G : SimpleGraph (Fin N),
    IsContained (completeGraph (Fin s)) G ∨
      IsContained (completeGraph (Fin t)) Gᶜ

Used by 2

Used byClassical Ramsey numbers · Classical Ramsey numbers as an infimum

DefinitionClassical Ramsey numbers#✓fully proved

For natural numbers \(s\) and \(t\), the Ramsey number \(R(s, t)\) is the least \(N\) such that every simple graph on \(N\) vertices contains the complete graph \(K_s\) as a subgraph or has a complement containing \(K_t\) as a subgraph, and \(0\) if there is no such \(N\).

Such an \(N\) always exists by the finite Ramsey theorem.

noncomputable def graphRamsey (s t : ℕ) : ℕ :=
  sInf {N : ℕ | classicalRamsey s t N}

def classicalRamsey (s t N : ℕ) : Prop :=
  ∀ G : SimpleGraph (Fin N),
    IsContained (completeGraph (Fin s)) G ∨
      IsContained (completeGraph (Fin t)) Gᶜ

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:40

Uses 1 · Used by 12

Statement usesThe Ramsey property for cliques

Used byClassical Ramsey numbers as an infimum · Burr–Erdős–Spencer leftover value · Exoo's lower bound for \(R(3, 10)\) · Exoo's lower bound for \(R(5, 5)\) · The Angeltveit–McKay upper bound for \(R(5, 5)\) · The value of \(R(4, 4)\) · The value of \(R(3, 8)\) · The value of \(R(3, 5)\) · The value of \(R(3, 9)\) · The value of \(R(3, 7)\) · The value of \(R(3, 6)\) · Angeltveit's upper bound for \(R(3, 10)\)

TheoremClassical Ramsey numbers as an infimum#✓fully proved

For all natural numbers \(s\) and \(t\), the Ramsey number \(R(s, t)\) equals the infimum in \(\mathbb{N}\) (where the empty set has infimum \(0\)) of the set of \(N\) such that every simple graph on \(N\) vertices contains the complete graph \(K_s\) as a subgraph or has a complement containing \(K_t\) as a subgraph.

theorem graphRamsey_eq_sInf (s t : ℕ) :
    graphRamsey s t = sInf {N : ℕ | classicalRamsey s t N}

noncomputable def graphRamsey (s t : ℕ) : ℕ :=
  sInf {N : ℕ | classicalRamsey s t N}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:50

def classicalRamsey (s t N : ℕ) : Prop :=
  ∀ G : SimpleGraph (Fin N),
    IsContained (completeGraph (Fin s)) G ∨
      IsContained (completeGraph (Fin t)) Gᶜ

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:40

Uses 2

Statement usesThe Ramsey property for cliques · Classical Ramsey numbers

DefinitionRamsey number of a pair of graphs#✓fully proved

For finite simple graphs \(G\) and \(H\), the Ramsey number \(R(G, H)\) is the least \(n\) such that every simple graph \(C\) on \(n\) vertices contains a copy of \(G\) as a subgraph or has a complement containing a copy of \(H\) as a subgraph, and \(0\) if there is no such \(n\).

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

Used by 5

Used byErdős Problem 570 (cycle versus graph Ramsey bound) · Diagonal Ramsey number of a graph · The pair Ramsey number as an infimum · Ramsey size linear graphs · Superlinear threshold for triangle-good graphs (Erdős Problem 1182)

TheoremThe pair Ramsey number as an infimum#✓fully proved

For finite simple graphs \(G\) and \(H\), the Ramsey number \(R(G, H)\) equals the infimum in \(\mathbb{N}\) (where the empty set has infimum \(0\)) of the set of \(n\) such that every simple graph \(C\) on \(n\) vertices contains a copy of \(G\) as a subgraph or has a complement containing a copy of \(H\) as a subgraph.

theorem graphPairRamsey_eq_sInf {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) :
    graphPairRamsey G H =
      sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:61

Uses 1

Statement usesRamsey number of a pair of graphs

DefinitionDiagonal Ramsey number of a graph#✓fully proved

For a finite simple graph \(G\), the diagonal Ramsey number of \(G\) is \(R(G, G)\): the least \(n\) such that for every simple graph \(C\) on \(n\) vertices, \(C\) or its complement contains a copy of \(G\) as a subgraph, and \(0\) if there is no such \(n\).

noncomputable def diagonalGraphRamsey {α : Type*} [Fintype α] (G : SimpleGraph α) : ℕ :=
  graphPairRamsey G G

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:61

Uses 1 · Used by 1

Statement usesRamsey number of a pair of graphs

Used byErdős Problem 800 on linear Ramsey numbers

DefinitionRamsey size linear graphs#✓fully proved

Let \(G\) be a finite simple graph. For a finite simple graph \(H\), write \(R(G, H)\) for the least \(m\) such that every simple graph on \(m\) vertices contains a copy of \(G\) or has a complement containing a copy of \(H\) (\(0\) if there is no such \(m\)), and write \(e(H)\) for the number of edges of \(H\). Then \(G\) is Ramsey size linear if there is a real constant \(c > 0\) such that for every \(n\) and every simple graph \(H\) on \(n\) vertices with no isolated vertices, \(R(G, H) \le c \cdot e(H)\).

def IsRamseySizeLinear {α : Type*} [Fintype α] (G : SimpleGraph α) : Prop :=
  ∃ c > (0 : ℝ), ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [DecidableRel H.Adj],
    (∀ v, 0 < H.degree v) →
    (graphPairRamsey G H : ℝ) ≤ c * H.edgeSet.ncard

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:61

Uses 1

Statement usesRamsey number of a pair of graphs

DefinitionErdős Problem 570 (cycle versus graph Ramsey bound)#✓fully proved

The statement that for every natural number \(k \ge 3\) there is an \(M\) such that for every \(m \ge M\) and every finite simple graph \(H\) with exactly \(m\) edges and no isolated vertices, the Ramsey number \(R(C_k, H)\) of the cycle \(C_k\) on \(k\) vertices and \(H\) is at most \(2m + \lfloor (k-1)/2 \rfloor\).

def conjecture : Prop :=
  ∀ (k : ℕ) (_ : 3 ≤ k),
    ∀ᶠ (m : ℕ) in atTop,
      ∀ (W : Type) [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj],
        (∀ v, 0 < H.degree v) →
        H.edgeSet.ncard = m →
        graphPairRamsey (cycleGraph k) H ≤ 2 * m + (k - 1) / 2

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:61

Uses 1 · Used by 1

Statement usesRamsey number of a pair of graphs

Used byResolution of Erdős Problem 570

TheoremResolution of Erdős Problem 570#●ready to prove

For every natural number \(k \ge 3\) there is an \(M\) such that for every \(m \ge M\) and every finite simple graph \(H\) with exactly \(m\) edges and no isolated vertices, the Ramsey number \(R(C_k, H)\) of the cycle \(C_k\) on \(k\) vertices and \(H\) is at most \(2m + \lfloor (k-1)/2 \rfloor\).

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∀ (k : ℕ) (_ : 3 ≤ k),
    ∀ᶠ (m : ℕ) in atTop,
      ∀ (W : Type) [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj],
        (∀ v, 0 < H.degree v) →
        H.edgeSet.ncard = m →
        graphPairRamsey (cycleGraph k) H ≤ 2 * m + (k - 1) / 2

WantedExt/Combinatorics/ErdosProblem570Wanted.lean:38

Sources

S. Cambie, A. Freschi, P. Morawski, K. Petrova, A. Pokrovskiy, Ramsey number of a cycle versus a graph of a given size, arXiv:2601.10238 (2026), https://arxiv.org/abs/2601.10238.

Uses 1

Statement usesErdős Problem 570 (cycle versus graph Ramsey bound)

DefinitionErdős Problem 800 on linear Ramsey numbers#✓fully proved

The proposition asserts that there is a real number \(C > 0\) such that for every natural number \(n\) and every simple graph \(G\) on \(n\) vertices in which no two adjacent vertices both have degree at least \(3\), the diagonal Ramsey number \(R(G, G)\) is at most \(Cn\).

def conjecture : Prop :=
  ∃ C > (0 : ℝ), ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
    Fintype.card V = n →
    (∀ u v, G.Adj u v → ¬(3 ≤ G.degree u ∧ 3 ≤ G.degree v)) →
    (SimpleGraph.diagonalGraphRamsey G : ℝ) ≤ C * n

Uses 1 · Used by 1

Statement usesDiagonal Ramsey number of a graph

Used byAlon's theorem on linear Ramsey numbers

TheoremAlon's theorem on linear Ramsey numbers#●ready to prove

There is a real number \(C > 0\) such that for every natural number \(n\) and every simple graph \(G\) on \(n\) vertices in which no two adjacent vertices both have degree at least \(3\), the diagonal Ramsey number \(R(G, G)\) is at most \(Cn\).

This answers Erdős Problem 800 affirmatively.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∃ C > (0 : ℝ), ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
    Fintype.card V = n →
    (∀ u v, G.Adj u v → ¬(3 ≤ G.degree u ∧ 3 ≤ G.degree v)) →
    (SimpleGraph.diagonalGraphRamsey G : ℝ) ≤ C * n

WantedExt/Combinatorics/ErdosProblem800Wanted.lean:32

Sources

Noga Alon, Subdivided graphs have linear Ramsey numbers, Journal of Graph Theory 18 (1994), 343–347, https://doi.org/10.1002/jgt.3190180406.

Uses 1

Statement usesErdős Problem 800 on linear Ramsey numbers

DefinitionSuperlinear threshold for triangle-good graphs (Erdős Problem 1182)#✓fully proved

The statement that for every real number \(C\), for all sufficiently large natural numbers \(n\), every connected graph \(G\) on the vertex set \(\{0, \dots, n - 1\}\) with at most \(Cn\) edges has \(R(K_3, G) = 2n - 1\). Here \(R(K_3, G)\) is the Ramsey number of the pair: the least \(N\) such that every graph on \(N\) vertices contains a triangle or has a complement containing a copy of \(G\).

This is the last question of Erdős Problem 1182, whether \(F(n) / n \to \infty\), where \(F(n)\) is the largest \(m\) such that every connected graph \(G\) on \(n\) vertices with at most \(m\) edges has \(R(K_3, G) = 2n - 1\); since this property is downward closed in \(m\), the two forms agree.

def triangleGoodnessSuperlinearThreshold : Prop :=
  ∀ C : ℝ, ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n), G.Connected →
    (G.edgeSet.ncard : ℝ) ≤ C * n →
    SimpleGraph.graphPairRamsey (⊤ : SimpleGraph (Fin 3)) G = 2 * n - 1

noncomputable def graphPairRamsey {α β : Type*} [Fintype α] [Fintype β]
    (G : SimpleGraph α) (H : SimpleGraph β) : ℕ :=
  sInf {n : ℕ | ∀ C : SimpleGraph (Fin n), G.IsContained C ∨ H.IsContained Cᶜ}

MathlibExt/Combinatorics/SimpleGraph/Ramsey.lean:61

Uses 1 · Used by 1

Statement usesRamsey number of a pair of graphs

Used byNo superlinear threshold for triangle-good graphs (Erdős Problem 1182)

TheoremNo superlinear threshold for triangle-good graphs (Erdős Problem 1182)#●ready to prove

It is not true that for every real number \(C\), for all sufficiently large natural numbers \(n\), every connected graph \(G\) on the vertex set \(\{0, \dots, n - 1\}\) with at most \(Cn\) edges has \(R(K_3, G) = 2n - 1\). Equivalently, there is a real number \(C\) such that for infinitely many \(n\) some connected graph \(G\) on \(\{0, \dots, n - 1\}\) with at most \(Cn\) edges has \(R(K_3, G) \ne 2n - 1\). Here \(R(K_3, G)\) is the Ramsey number of the pair: the least \(N\) such that every graph on \(N\) vertices contains a triangle or has a complement containing a copy of \(G\), and \(0\) if there is no such \(N\).

Brandt proved \(F(n) \le 84n\), where \(F(n)\) is the largest \(m\) such that every connected graph on \(n\) vertices with at most \(m\) edges has \(R(K_3, G) = 2n - 1\). So for all large \(n\) some connected graph on \(n\) vertices with at most \(84n + 1\) edges has \(R(K_3, G) \ne 2n - 1\), and the statement fails for \(C = 85\). Brandt's 1996 preprint is unrefereed; erdosproblems.com/1182 accepts it.

public theorem_wanted triangleGoodnessSuperlinearThreshold_refuted :
    ¬ triangleGoodnessSuperlinearThreshold

def triangleGoodnessSuperlinearThreshold : Prop :=
  ∀ C : ℝ, ∀ᶠ n : ℕ in atTop, ∀ G : SimpleGraph (Fin n), G.Connected →
    (G.edgeSet.ncard : ℝ) ≤ C * n →
    SimpleGraph.graphPairRamsey (⊤ : SimpleGraph (Fin 3)) G = 2 * n - 1

WantedExt/Combinatorics/TriangleGoodSparseConnectedGraphsErdosProblem1182Wanted.lean:50

Sources

T. F. Bloom, Erdős Problems, Problem #1182, https://www.erdosproblems.com/1182 (status OPEN); resolution: S. Brandt, Expanding graphs and Ramsey numbers, preprint, Serie A Mathematik, Freie Universität Berlin, 1996 (unrefereed; accepted on erdosproblems.com/1182), F(n) ≤ 84n, as recorded on erdosproblems.com/1182: 'The upper bound was improved to F(n) ≤ 84n by Brandt ... (This resolves the final question in the negative.)', https://ftp.math.fu-berlin.de/pub/math/publ/pre/1996/pr-a-96-24.ps.

Uses 1

Statement usesSuperlinear threshold for triangle-good graphs (Erdős Problem 1182)

10 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.