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

Pjotr Buys, Sven Polak, Jeroen Zuiddam

arXiv:2607.29681v1 Primary: math.CO Secondary: cs.IT

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.

Disclosure

“g constructions for powers of odd cycles go back to Baumert, McEliece, Rodemich, Rumsey, Stanley and Taylor [BMR+ 71]. Recently, [IRCR26, Gao26] used large language models to obtain improved lower bounds on Shannon capacity of small odd cycles. Following their methods and using ChatGPT 5.6 Sol Pro and Claude Opus 5 we find”
PDF page 1

Classification: Substantial mathematical content or result generation
Multiplier: 10
Verified: 2026-08-23T19:16:17.994633Z

Structural counts

Pages 4 pdf

Theorems 1 source

Lemmas 0 source

Propositions 0 source

Corollaries 0 source

Definitions 0 source

Displayed equations 2 source

Bibliography entries 14 source

Appendix pages 0 estimated

Count notes

Source counts use the expanded primary TeX file main3.tex.
Appendix pages include the first PDF page with an explicit Appendix heading through the final page.