PODC 2026 · 45th ACM Symposium on Principles of Distributed Computing, Egham, United Kingdom, July 2026
We show that there is a one-round randomized distributed algorithm that can 2-color cycles such that the expected fraction of monochromatic edges is less than $0.24118$. We also show that a one-round algorithm cannot achieve a fraction less than $0.23879$. Before this work, the best upper and lower bounds were $0.25$ and $0.2$. Our proof was largely discovered and developed by large language models, and both the upper and lower bounds have been formalized in Lean 4.