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)\geq3.258805369885\ldots$, $\Theta(C_{11})\geq5.294502522149\ldots$, $\Theta(C_{13})\geq6.302455083464\ldots$, $\Theta(C_{15})\geq7.301600534487\ldots$, $\Theta(C_{19})\geq9.357192705918\ldots$, $\Theta(C_{21})\geq10.342455853338\ldots$, and $\Theta(C_{23})\geq11.328224257774\ldots$. 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.