{"id":"palomar/PALOMAR-2026-10-13-000006","url":"https://github.com/linrock/math-proofs/tree/ba96303b34a95ac458958c1eb0bbdee54733484a/erdos-1105","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000006-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.CO","msc:05C55","msc:05C38","msc:05C35","extremal-combinatorics","anti-ramsey","lean"],"score":0,"title":"Erdős 1105: anti-Ramsey numbers for cycles and paths","trust":"high","domain":"math.CO","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 proof of both parts of Erdős problem 1105 on the anti-Ramsey number AR(n, H), the maximum number of colors in a surjective edge-coloring of K_n with no rainbow copy of H. Part (i) proves the Erdős–Simonovits–Sós (1975) cycle formula AR(n, C_k) = ((k - 2) / 2 + 1 / (k - 1)) n + O(1) for every fixed k ≥ 3 (Montellano-Ballesteros and Neumann-Lara 2005; Choi 2011), together with the exact triangle value AR(n, C_3) = n - 1 and the explicit two-sided bounds ⌊n / (k - 1)⌋(choose(k - 1, 2) + 1) - 1 ≤ AR(n, C_k) ≤ ((k - 2) / 2 + 1 / (k - 1)) n - 1 for all n ≥ k ≥ 3 via private-color…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-13","reactions":{},"formalized":true,"formalizes":[{"title":"Anti-Ramsey theorems","identifier":"https://real.mtak.hu/110457/1/1975-05.pdf","relationship":"formalizes"},{"title":"An anti-Ramsey theorem on cycles","identifier":"https://doi.org/10.1007/s00373-005-0619-3","relationship":"adapts"},{"title":"Problems in Graph Theory and Probability","identifier":"https://doi.org/10.31274/etd-180810-2269","relationship":"adapts"},{"title":"The anti-Ramsey number for paths","identifier":"https://arxiv.org/abs/2102.00807","relationship":"adapts"}]}