Erdős problem 617 · problems.science

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}$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

617.lean

Retained formal statement3 of 4

Erdős and Gyárfás [ErGy99] proved the conjecture for $r=4$ .

FormalConjectures/ErdosProblems/617.leanErdos617.erdos_617.variants.r_eq_44 linesExact file

1∀ r ≥ 3,2  ∀ {V : Type} [inst : Fintype V] [DecidableEq V],3    Fintype.card V = 4 ^ 2 + 1 →4      ∀ (coloring : Sym2 V → Fin 4), ∃ S k, S.card = 4 + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

SolvedStatement only, no proof

Sources

Search problems.science