The Shannon capacity of odd cycles of length at least seven is unknown, and improving rigorous lower bounds requires large explicit independent sets in strong powers whose correctness is hard to verify by hand.

An iterative star-product procedure on valid tuples (Gao's gadget construction) is used to build large independent sets in strong powers of odd cycles from computationally discovered base tuples. Base tuples for C7, C11, C13, C15, C19, C21, C23 were obtained using large language models. The base tuples and their validity proofs are encoded as explicit literals in Lean, which checks that each is valid.

New lower bounds are established, e.g. Θ(C7) ≥ 3.258805..., Θ(C11) ≥ 5.294502..., and Θ(C13) ≥ 6.302455..., improving prior bounds; all bounds are fully formalised and verified in Lean.