Small Ramsey numbers

TheoremThe value of \(R(4, 4)\)#●ready to prove

The classical Ramsey number \(R(4, 4)\) equals \(18\).

public theorem_wanted graphRamsey_four_four : graphRamsey 4 4 = 18
Sources
  • R. E. Greenwood and A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955), 1–7; S. P. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1; listed in leansolving/SqueezeBench SqueezeBench/Problems/Ramsey/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremExoo's lower bound for \(R(5, 5)\)#●ready to prove

The classical Ramsey number \(R(5, 5)\) is at least \(43\).

Thus some simple graph on \(42\) vertices contains no \(K_5\) and no independent set of size \(5\).

public theorem_wanted forty_three_le_graphRamsey_five_five : 43 ≤ graphRamsey 5 5
Sources
  • G. Exoo, A lower bound for R(5,5), J. Graph Theory 13 (1989), 97–98; Radziszowski, DS1; listed in SqueezeBench SqueezeBench/Problems/Ramsey/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe Angeltveit–McKay upper bound for \(R(5, 5)\)#●ready to prove

The classical Ramsey number \(R(5, 5)\) is at most \(46\).

public theorem_wanted graphRamsey_five_five_le_forty_six : graphRamsey 5 5 ≤ 46
Sources
  • V. Angeltveit and B. D. McKay, R(5,5) ≤ 46, arXiv:2409.15709 (2024); listed in SqueezeBench SqueezeBench/Problems/Ramsey/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe value of \(R(3, 5)\)#●ready to prove

The classical Ramsey number \(R(3, 5)\) equals \(14\).

public theorem_wanted graphRamsey_three_five : graphRamsey 3 5 = 14
Sources
  • Greenwood and Gleason (1955), op. cit.; Radziszowski, DS1; OEIS A000791; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe value of \(R(3, 6)\)#●ready to prove

The classical Ramsey number \(R(3, 6)\) equals \(18\).

public theorem_wanted graphRamsey_three_six : graphRamsey 3 6 = 18
Sources
  • G. Kéry, On a theorem of Ramsey, Mat. Lapok 15 (1964), 204–224 (upper bound), with the lower bound from Kalbfleisch (1966); Radziszowski, DS1; OEIS A000791; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe value of \(R(3, 7)\)#●ready to prove

The classical Ramsey number \(R(3, 7)\) equals \(23\).

public theorem_wanted graphRamsey_three_seven : graphRamsey 3 7 = 23
Sources
  • J. G. Kalbfleisch, Chromatic graphs and Ramsey's theorem, Ph.D. thesis, University of Waterloo (1966) (lower bound); J. E. Graver and J. Yackel, Some graph theoretic results associated with Ramsey's theorem, J. Combin. Theory 4 (1968), 125–175 (upper bound); Radziszowski, DS1; OEIS A000791; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe value of \(R(3, 8)\)#●ready to prove

The classical Ramsey number \(R(3, 8)\) equals \(28\).

public theorem_wanted graphRamsey_three_eight : graphRamsey 3 8 = 28
Sources
  • C. Grinstead and S. Roberts, On the Ramsey numbers R(3,8) and R(3,9), J. Combin. Theory Ser. B 33 (1982), 27–51 (lower bound); B. D. McKay and Zhang Ke Min, The value of the Ramsey number R(3,8), J. Graph Theory 16 (1992), 99–105 (upper bound); Radziszowski, DS1; OEIS A000791; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremThe value of \(R(3, 9)\)#●ready to prove

The classical Ramsey number \(R(3, 9)\) equals \(36\).

public theorem_wanted graphRamsey_three_nine : graphRamsey 3 9 = 36
Sources
  • Kalbfleisch (1966), op. cit. (lower bound); Grinstead and Roberts (1982), op. cit. (upper bound); Radziszowski, DS1; OEIS A000791; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremExoo's lower bound for \(R(3, 10)\)#●ready to prove

The classical Ramsey number \(R(3, 10)\) is at least \(40\).

public theorem_wanted forty_le_graphRamsey_three_ten : 40 ≤ graphRamsey 3 10
Sources
  • G. Exoo, On two classical Ramsey numbers of the form R(3,n), SIAM J. Discrete Math. 2 (1989), 488–490; Radziszowski, DS1; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers

TheoremAngeltveit's upper bound for \(R(3, 10)\)#●ready to prove

The classical Ramsey number \(R(3, 10)\) is at most \(41\).

public theorem_wanted graphRamsey_three_ten_le_forty_one : graphRamsey 3 10 ≤ 41
Sources
  • V. Angeltveit, R(3,10) ≤ 41, arXiv:2401.00392 (2024); Radziszowski, DS1; listed in SqueezeBench SqueezeBench/Problems/Ramsey3/README.md.
Uses 1
Statement usesClassical Ramsey numbers
10 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.