Formalizes in Lean 4 both upper and lower bounds for one-round randomized 2-coloring of cycles.
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.
Problem
For randomized one-round distributed algorithms that 2-color directed cycles, the best known bounds on the minimum achievable fraction of monochromatic edges p* were 0.2 (lower) and 0.25 (upper).
Approach
The authors study the problem by analyzing 3-dimensional De Bruijn graphs in two variants (normal and distinct). Upper bounds come from explicit coloring algorithms parameterized by thresholds; lower bounds come from linear programming relaxations on the distinct De Bruijn graph. Both bounds are formalized in Lean 4. The proof was largely discovered and developed by large language models.
(b) The three-parameter algorithm f that achieves p(f)<0.24118 .
Results
The achievable fraction of monochromatic edges is bounded as 0.23879 <= p* < 0.24118, substantially tightening both the previous upper and lower bounds.
