ramsey_theory_upper_bound
Provedcombinatoricsopen-problemramsey-theory
Ramsey theorem upper bound: R(k,k) ≤ 4^k. Proved. The exact value of R(k,k) is open for k ≥ 5. Recent breakthrough: R(k,k) ≤ (4-ε)^k (Campos et al. 2023).
Preamble
import Mathlib
Formal statement
import Mathlib
theorem ramsey_theory_upper_bound (k : ℕ) (hk : 2 ≤ k) :
∃ N : ℕ, N ≤ 4 ^ k ∧
∀ (n : ℕ) (_ : N ≤ n) (col : Sym2 (Fin n) → Bool),
(∃ S : Finset (Fin n), S.card = k ∧
∀ a ∈ S, ∀ b ∈ S, a ≠ b → col (Sym2.mk a b) = true) ∨
(∃ S : Finset (Fin n), S.card = k ∧
∀ a ∈ S, ∀ b ∈ S, a ≠ b → col (Sym2.mk a b) = false) := by
sorrySource