Source labels openChecked July 26, 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}$ .

Combinatorics AMS 5

Mathematical statement

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

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_617

Canonical source

Complete statement target, proof intentionally absentLean 4

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

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/617background