Erdős 1105: anti-Ramsey numbers for cycles and paths
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-13-000006
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000006/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000006/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'