Lean-verified lower bounds for the Shannon capacity of odd cycles
2026-07-31 • Information Theory
Information Theory
AI summaryⓘ
The authors provide new, improved minimum values for the Shannon capacities of certain small odd cycle graphs, specifically for cycles with 7, 11, 13, 15, 19, 21, and 23 nodes. These capacities measure the maximum rate of information that can be transmitted without error over a channel modeled by these graphs. The results were achieved using an iterative mathematical method developed by Gao, which itself builds on earlier work by Itty and colleagues. The authors also verified their results rigorously using the Lean proof assistant software.
Shannon capacityodd cyclegraph theoryiterative methodinformation theorylower boundsformal verificationLean proof assistant
Authors
Pjotr Buys, Sven Polak, Jeroen Zuiddam
Abstract
We give new lower bounds for the Shannon capacities of small odd cycles: $Θ(C_7)\geq3.258805369885\ldots$, $Θ(C_{11})\geq5.294502522149\ldots$, $Θ(C_{13})\geq6.302455083464\ldots$, $Θ(C_{15})\geq7.301600534487\ldots$, $Θ(C_{19})\geq9.357192705918\ldots$, $Θ(C_{21})\geq10.342455853338\ldots$, and $Θ(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.