Erdős-Gyárfás Balanced Five-Colorings
Abstract
A coloring of the edges of a complete graph with r colors is balanced if the edges among any r+1 vertices use all r colors. Erdős and Gyárfás (1999) conjectured that for all r≥3 the complete graph Kr2+1 has no balanced r-coloring. They proved the conjecture for r=3 and r=4. We prove the conjecture for r=5, the first new case settled in over two decades. There is no balanced $5$-coloring of K26, and since K25 has one, K25 is the largest complete graph admitting a balanced $5$-coloring. We design a reduce--dispatch--enumerate workflow, where every machine step produces an artifact that can be independently checked. First, we use a machine-checked (Lean 4) proof to reduce the conjecture to a single extremal statement about the color class with the fewest edges: no graph on $26$ vertices has between $55$ and $65$ edges while every $6$ of its vertices span between $1$ and $11$ edges. We then search on the sparse class instead of its dense complement, which makes enumeration up to isomorphism feasible. With classical stability theorems for K6-free graphs, we dispatch the five near-extremal edge counts analytically. For the exhaustive enumeration on the remaining six edge counts, we design efficient encodings with SAT modulo symmetries and parallel cube-and-conquer. We also certify all eleven edge counts: each of the 12,296 subproblems carries a clausal refutation checked by the independent verifier drat-trim, and all 273,503,938 symmetry-breaking clauses are also validated against the vertex permutations that justify them.
Related
BibTeX
@misc{xia2026erdősgyárfás,
title = {{Erdős-Gyárfás Balanced Five-Colorings}},
author = {Hai Xia and Stefan Szeider},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.24484},
eprint = {2610.24484},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.24484},
}
RIS
TY - UNPB
TI - Erdős-Gyárfás Balanced Five-Colorings
AU - Hai Xia
AU - Stefan Szeider
PY - 2026
DA - 2026/10/17
PB - arXiv
DO - 10.48550/arxiv.2610.24484
UR - https://arxiv.org/abs/2610.24484
AB - A coloring of the edges of a complete graph with r colors is balanced if the edges among any r+1 vertices use all r colors. Erdős and Gyárfás (1999) conjectured that for all r≥3 the complete graph K_r^2+1 has no balanced r-coloring. They proved the conjecture for r=3 and r=4. We prove the conjecture for r=5, the first new case settled in over two decades. There is no balanced $5$-coloring of K_26, and since K_25 has one, K_25 is the largest complete graph admitting a balanced $5$-coloring. We design a reduce--dispatch--enumerate workflow, where every machine step produces an artifact that can be independently checked. First, we use a machine-checked (Lean 4) proof to reduce the conjecture to a single extremal statement about the color class with the fewest edges: no graph on $26$ vertices has between $55$ and $65$ edges while every $6$ of its vertices span between $1$ and $11$ edges. We then search on the sparse class instead of its dense complement, which makes enumeration up to isomorphism feasible. With classical stability theorems for K_6-free graphs, we dispatch the five near-extremal edge counts analytically. For the exhaustive enumeration on the remaining six edge counts, we design efficient encodings with SAT modulo symmetries and parallel cube-and-conquer. We also certify all eleven edge counts: each of the 12,296 subproblems carries a clausal refutation checked by the independent verifier drat-trim, and all 273,503,938 symmetry-breaking clauses are also validated against the vertex permutations that justify them.
ER -