Claude 与 Lean 辅助重新划定二部图 k-star-forming 数猜想：一般反例、链图成立与 NP 完全性

Deep Bhattacharjee 于 10 月 23 日研究 Sahbi 的 k-star-forming / k-independence 猜想，报告对每个 k≥3 构造 3k+3 个顶点的连通二部图，满足 β_k=2k+2 而 upper star-forming 数至少 3k，否定二部图一般等式；同时证明链图的等式对所有 k 成立，并将二部图 minimal 2-star-forming 集合大小判定问题证明为 NP-complete。Claude Code/Opus 5.5 负责搜索、程序、Lean 4 证明和初稿，作者指导并批准；公开版本化源码，但没有独立专家审稿。原文还提及相关前期公开的小参数反例，因此本记录主要是全 k 家族与复杂性结论的新发表，而非首个小实例。