The Burr-Erdős-Graham-Sós conjecture concerns the number of colors needed to force copies of an odd cycle graph to be rainbow
subgraphs. For a graph 
, let 
be the least number of colors in an edge
coloring of some graph on 
vertices with at least 
edges in which every copy of 
is a rainbow subgraph.
The conjecture states that, for every fixed integer 
,
 |
as 
,
where 
is the floor function (Burr et al. 1989).
Bucić et al. (2026) proved the conjecture for 
. Shahab (2026) proved the remaining case 
, corresponding to the cycle graph 
,
and therefore completed the proof. The conjecture is numbered 809
in the Erdős problems collection (Bloom 2026).
Shahab (2026) reports that agents based on OpenAI Codex and Anthropic Claude were used in the search for the proof, construction of the exact rational certificate, Lean formalization, and preparation of the manuscript. A finite counting lemma was proved with assistance from Harmonic's Aristotle. The author assumes responsibility for the paper, and the stated results are checked by the accompanying Lean development.
