Claude 辅助分类圆形二进制词中最少 abelian squares 的全部极端情形，报告六项 Lean 核验定理

Deep Bhattacharjee 于 10 月 22 日发表关于长度 n 的 binary circular words 中 distinct abelian squares 数量的研究，报告下界 ⌊(n−1)/2⌋ 并完整分类取等词，修正 Simpson 猜想在特定偶数长度时遗漏交替词 (ab)^(n/2) 的部分。Claude Code 参与检索、证明、Lean 4 工件与程序核验，作者称六项主要结论均在 Lean/Mathlib 内闭合，且由 C、C++、Python、Julia 等多实现检查小规模情形。本轮不将有限实例检查误写为无限情形的机器独立证明。