The Burr-Erdős-Graham-Sós conjecture for the seven-cycle
Asad Shahab
math.CO
Sep 29, 2026 · v1
TL;DR
Formalizes in Lean 4 the Burr-Erdős-Graham-Sós rainbow odd-cycle conjecture for all k≥3, including the new seven-cycle proof and the Bucić-Chen-Ma argument.
Abstract
For a graph $H$, let $f(n,e,H)$ be the least number of colors in an edge-coloring of some $n$-vertex graph with at least $e$ edges in which every copy of $H$ is rainbow. Burr, Erdős, Graham, and Sós conjectured that $f(n,\lfloor n^2/4\rfloor+1,C_{2k+1})=(1/8+o(1))n^2$ for every fixed $k\ge3$, and Bucić, Chen, and Ma recently proved this for all $k\ge4$. We prove the remaining case $k=3$: \[ f\left(n,\left\lfloor n^2/4\right\rfloor+1,C_7\right) =\left(\frac18+o(1)\right)n^2. \] The lower bound rests on a weighted palette inequality, which we prove with an exact rational certificate on five sampled vertices. Its main ingredients are a fractional matching of compatible triangular edges and private resources attached to nontriangular edges. A stable form of the inequality, combined with regularity, triangle removal, and a direct argument for graphs close to bipartite, transfers the bound to arbitrary edge-colorings. We also describe a Lean 4 formalization of the conjecture for every fixed $k\ge3$, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for $k\ge4$.
Problem
Burr, Erdős, Graham, and Sós conjectured that the minimum number of colors needed to make every C_{2k+1} rainbow in some n-vertex graph with ⌊n²/4⌋+1 edges is (1/8+o(1))n² for every fixed k≥3. Bucić, Chen, and Ma proved the cases k≥4, leaving k=3, the seven-cycle, open.
Approach
The lower bound rests on a weighted palette inequality, proved by an exact rational polynomial certificate on five sampled vertices verified by computer. The inequality uses a fractional matching of compatible triangular edges and private resources attached to nontriangular edges. A stable form of the inequality is transferred to arbitrary edge-colorings using regularity, triangle removal, and a direct argument for graphs close to bipartite. The full conjecture for every k≥3 is formalized in Lean 4, combining the seven-cycle proof with a formalization of the Bucić-Chen-Ma argument.
Results
The case k=3 is settled: f(n,⌊n²/4⌋+1,C_7)=(1/8+o(1))n², which completes the conjecture (Erdős Problem #809) for all fixed k≥3. A Lean 4 formalization covers the full statement.
