2-Coloring Cycles in One Round

TL;DR

This paper presents new bounds for one-round randomized algorithms to 2-color cycles, achieving a lower expected monochromatic edge fraction than previous bounds, with proofs developed using language models and formalized in Lean 4.

Contribution

It introduces improved upper and lower bounds for one-round 2-coloring of cycles, utilizing language models and formal verification.

Findings

Expected monochromatic edges less than 0.24118 with a new algorithm

Lower bound of 0.23879 for any one-round algorithm

Previous bounds were 0.25 and 0.2

Abstract

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.