Lean-verified lower bounds for the Shannon capacity of odd cycles

Abstract

We give new lower bounds for the Shannon capacities of small odd cycles: $\Theta (C_7)\ge 3.258805369885\dots$, $\Theta (C_{11})\ge 5.294502522149\dots$, $\Theta (C_{13})\ge 6.302455083464\dots$, $\Theta (C_{15})\ge 7.301600534487\dots$, $\Theta (C_{19})\ge 9.357192705918\dots$, $\Theta (C_{21})\ge 10.342455853338\dots$, and $\Theta (C_{23})\ge 11.328224257774\dots$. The bounds are obtained by an iterative procedure due to Gao (2026) which is based on a method by Itty, Rosin, Carstensen and Reichman (2026). The bounds are fully formalised in Lean.