Lean验证的奇环香农容量下界
Lean-verified lower bounds for the Shannon capacity of odd cycles
浏览论文内容
中文总结 AI 辅助
该研究通过Gao的迭代程序，结合Itty等人的方法，在Lean中形式化得到了小型奇环C₇、C₁₁等的香农容量新下界。
中文摘要 AI 辅助
我们给出了小型奇环的香农容量新下界：Θ(C₇)≥3.258805369885…，Θ(C₁₁)≥5.294502522149…，Θ(C₁₃)≥6.302455083464…，Θ(C₁₅)≥7.301600534487…，Θ(C₁₉)≥9.357192705918…，Θ(C₂₁)≥10.342455853338…，Θ(C₂₃)≥11.328224257774…。这些下界由Gao（2026）提出的迭代程序得到，该程序基于Itty、Rosin、Carstensen和Reichman（2026）的方法，且已在Lean中完全形式化。
英文摘要
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.
