Balanced $r$-colourings of $K_{r^2+1}$: must some $K_{r+1}$ miss a colour? (Erdős #617)
Statement
Let $r\geq 3$. Call an $r$-colouring of the edges of a complete graph *balanced* if every set of $r+1$ vertices induces a $K_{r+1}$ whose edges carry all $r$ colours. The conjecture: 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}$ — equivalently, $K_{r^2+1}$ admits NO balanced $r$-colouring for any $r\geq 3$. A single explicit balanced $r$-colouring of $K_{r^2+1}$ for some $r\geq 5$ would disprove it.
Acceptance. FULLY RESOLVES (disproof): a specific $r\geq 5$ together with an explicit $r$-colouring of the edges of $K_{r^2+1}$ (adjacency-list or matrix file) plus verification code that enumerates all $\binom{r^2+1}{r+1}$ subsets of size $r+1$ and certifies every one induces all $r$ colours — fully machine-checkable. FULLY RESOLVES (proof): a proof that for every $r\geq 3$ no balanced $r$-colouring of $K_{r^2+1}$ exists; machine-checkable (Lean, against the existing formal-conjectures statement) preferred, else a complete written proof. ADVANCES: settle a new individual value of $r$ beyond the known $r=3,4$ — e.g. an exhaustive SAT/CP resolution of $r=5$ ($K_{26}$) with a reproducible UNSAT certificate (DRAT or equivalent) or an explicit balanced colouring; or a structural theorem constraining balanced colourings (e.g. forcing near-affine-plane structure) that reduces the search space, with proof. Deliver the colouring file + checker, or the SAT encoding + certificate, or the proof file.
Background
A conjecture of Erdős and Gyárfás [ErGy99], also raised by Erdős [Er99]; listed as open on erdosproblems.com/617 (fetched 2026-07-13, status 'falsifiable' — open, but a finite counterexample would disprove it). Known frontier, all from Erdős–Gyárfás: the conjecture is TRUE for $r=3$ and $r=4$ (proved in [ErGy99]); it is FALSE for $r=2$ (a balanced 2-colouring of $K_5$ exists); and the vertex count $r^2+1$ is sharp in a strong sense — if $r^2+1$ is replaced by $r^2$, balanced $r$-colourings exist for infinitely many $r$. So the first genuinely open case is $r=5$: does $K_{26}$ admit a 5-colouring in which every 6-clique sees all 5 colours? A formal Lean statement of the problem already exists in the google-deepmind/formal-conjectures repository. The venue hosts several Ramsey-number problems (e.g. small Ramsey records, $R(3,3,3,3)$); this balanced-colouring variant is related in flavour but distinct. The attacker's tools: for $r=5$ the instance is finite and SAT-shaped — 325 edges, 5 colours, and one 'colour $c$ appears in $S$' clause for each of the $\binom{26}{6}=230{,}230$ six-subsets and each colour (about $1.15$M clauses over ~1,625 one-hot variables) — so a SAT/CP search with symmetry breaking can either exhibit a balanced colouring (disproof) or, with a DRAT/verified UNSAT certificate, settle $r=5$; algebraic constructions (the known $K_{r^2}$ balanced colourings) are natural seeds for local search at larger $r$.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #617 (T. F. Bloom) | website |
| REF-02 | Formal Lean statement of Erdős #617 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.