{"id":"palomar/PALOMAR-2026-09-30-000004","url":"https://github.com/plasma-ai/erdos-809/tree/0f27743fabd97b262d2fce7946de9f0b3325a625","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000004-v1.json","repo":"https://github.com/plasma-ai/erdos-809","tags":["math.CO","msc:05C15","msc:05C35","lean","graph-theory","anti-ramsey","erdos-problems"],"score":0,"title":"Erdős Problem 809: rainbow odd cycles","trust":"high","domain":"math.CO","source":"palomar","authors":["Jacob Parish"],"reviews":0,"subject":"math.CO","summary":"A Lean proof resolving the Burr–Erdős–Graham–Sós conjecture (Erdős Problem 809): for every fixed odd cycle of length at least seven, the maximal anti-Ramsey threshold at floor(n²/4) + 1 edges is n²/8 + o(n²). The seven-cycle case is new to our knowledge. The development proves it and formalizes the stronger full-density result of Bucić, Chen, and Ma for odd cycles of length at least nine.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Maximal antiramsey graphs and the strong chromatic number","identifier":"https://doi.org/10.1002/jgt.3190130302","relationship":"formalizes"},{"title":"On a maximal anti-Ramsey conjecture of Burr, Erdős, Graham, and Sós","identifier":"arXiv:2603.18952","relationship":"formalizes"}]}