arXiv++ Combinatorics

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\ge3$ 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.

We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and human strategic direction, jointly produced a new result in combinatorial design theory. The main result of this human-AI collaboration is a tight lower bound on the imbalance of Latin squares for the notoriously difficult case $n \equiv 1 \pmod{3}$. We reconstruct the discovery process from detailed interaction logs spanning multiple sessions over several days and identify the distinct cognitive contributions of each component. The AI agent proved effective at uncovering hidden structure and generating hypotheses. The symbolic component consists of computer algebra, constraint solvers, and simulated annealing, which provides rigorous verification and exhaustive enumeration. Human steering supplied the critical research pivot that transformed a dead end into a productive inquiry. Our analysis reveals that multi-model deliberation among frontier LLMs proved reliable for criticism and error detection but unreliable for constructive claims. The resulting human-AI mathematical contribution, a tight lower bound of $4n(n{-}1)/9$, is achieved via a novel class of near-perfect permutations. The bound was formally verified in Lean 4. Our experiments show that neurosymbolic systems can indeed produce genuine discoveries in pure mathematics.