Erdős Problem 617

Conjecture 617 · Erdős

Let $r\geq 3$ . If the edges of $K_{r^2+1}$ are $r$ -coloured then there exist $r+1$ vertices with at least one colour missing on the edges of the induced $K_{r+1}$ .

In other words, there is no balanced colouring.

A conjecture of Erdős and Gyárfás [ErGy99].

Formal statement · Lean 4.lean

theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V]
    (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) :
    ∃ (S : Finset V) (k : Fin r),
      S.card = r + 1 ∧
      ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗