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.

翻译：我们证明存在一种单轮随机化分布式算法，能够对环进行二着色，使得单色边的期望比例小于0.24118。同时，我们证明单轮算法无法实现小于0.23879的比例。在本研究之前，最佳上界和下界分别为0.25和0.2。我们的证明主要由大语言模型发现和构建，且上下界结果均在Lean 4中完成了形式化验证。