Combinatorics

Erdős 617

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].

References

erdosproblems.com/617

ErGy9900323-9) Erdős, Paul and Gyárfás, András, Split and balanced colorings of complete graphs. Discrete Math. (1999), 79-86.

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«617»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos617.erdos_617" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/617.lean

Source type SHA-256: sha256:21890d8a7a194e61d643ac6026bd6c04481a9503619752d21f1a4b1160032eb8
Task id: fc-379fc029-erdos617-erdos-617-7b45b4e8fd-formalized-v1
Task commitment: sha256:9bd71ec9d2dc4a50134ff3318fa5318576811db06c67920c4eb1116fa55d61d1

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.