AI 辅助证明循环旋转集合覆盖问题 NP 完全，Lean 核验算法归约与复杂性论证

YURAN XIU 在 Hexagon 发表此前 WADS 2023 所提 Set-Cover by Rotations 问题的复杂性结果：给定显式二进制模式与预算，判定若干循环移位能否覆盖全部位置是 NP-complete。文章通过 replicated-marker 和环图编码建立 3-SAT 的多项式归约，称 Lean 形式化涵盖数学归约、完整字串算法、NP membership 与无条件 NP-hardness 基础，并提供 HAL 归档。条目为主要 AI 生成，贡献者未声称已经完成人类数学审稿。