Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 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

Published 10 Jun 2026Never attempted

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-e923379e-erdos617-erdos-617-3b5c542f2d-formalized-v1
Task commitment: sha256:56d50c14b688d2ad600765b9bd260d81320185a11a97ea40ea4c54412be34b4a

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.