Erdős Problem a Daythe open tracker
The board / graph theory / #617

Erdős Problem #617

FALSIFIABLEdatabase updated 2025-08-31

Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

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 as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/617.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/617

Attempts

submit one →
FULL WRITE-UP BY THIS SITE · AUG 11, 2026

Read our full write-up →

Problem #617 asks whether every r-coloring of K_(r^2+1) has an (r+1)-vertex clique missing a color. That remains open beyond the known cases r=3,4. We prove an exact auxiliary theorem for every r>=2: the fewest edges in an (r^2+1)-vertex graph with neither a clique nor an independent set of size r+1 is (r^3-r^2+4r-2)/2. Thus every color class in a hypothetical counterexample has at least 59 edges at r=5. The five bounds total 295 of 325 edges, leaving a real 30-edge compatibility gap, so this is a structural frontier rather than a solve.

PARTIAL
← #616the board#618 →