GPT-6 Astra 联手数学爱好者，证明 57 年「摆圆」难题

一个长期研究数学、机器学习和优化算法的技术作者 nor，用 GPT-6 Astra 把一道半个多世纪悬而未决的几何难题向前推进了一大步。他借助模型，为 15、16、17、18 和 20 个等半径圆盘「装进最小外圆」的排列给出了严格的最优性证明。此前，数学界只对 N≤14 和 N=19 的情形做过严格验证。

这道题的第一层是找出最好的摆法，真正困难的是第二层：严格证明没有比它更好的摆法。1968 年，美国数学家葛立恒（Graham）证明了 N≤7 的情形；1969 年，研究者 Udo Pirl 把范围推进到 10 个圆盘，并研究了 11 到 19 个圆盘的排列方案。直到 2003 年前后，N≤14 与 N=19 才被严格证明。

按照量子位的报道，nor 的做法是循序渐进的：先让 GPT-6 Astra 处理 N=15，模型解决之后，再让它把同一套方法推广到 16、17，以及 18 和 20，这些情况下模型都成功给出了证明结果。文中也提到，N 到 20 并不是模型的极限，只是 nor 没有再继续往下证。

GPT-6 Astra 的核心思路，是不再直接搜索最优解，而是借助几何约束把无限多种可能排列收缩为有限情形，再交给计算机逐一排除，最终严格证明经典排列已经最优。

整个证明被拆成五步：证明在一定条件下可以把靠近外圆的圆盘向外移动而不引起重叠；利用圆盘之间必须保持的角度间隔，把角度总和超过 360° 的排列直接排除；不再搜索每个圆盘的具体坐标，而是检查圆盘到圆心的距离区间及其环绕次序；再利用接触约束证明可行排列无法发生符合条件的微小形变，从而把「非常接近」提升为「严格一致」（15 个圆盘的情况另用奇数环论证）；最后证明原始排列中必然至少有一个圆盘接触外圆边界，这意味着不可能把它们塞进半径更小的外圆。

值得注意的是，这并不是 nor 给出一轮提示词、模型就一次完成。nor 在博客中写道，他作为人类的贡献包括：确定问题的可行性、引导模型、与漏洞百出的网页界面作斗争、忍受糟糕的文案、修复细微问题、反复推敲表述、手动验证其有效性，并用 Astra 和 Opus 5.5 重新检查了全部内容。

这个案例之所以值得关注，是因为它再次显示 AI 正从「解题」走向「严格证明」：把原本需要人类数学家长期打磨的最优性论证，压缩到可被机器逐一验证的有限搜索之中。模型在这里更像放大器——人类负责提出问题、判断可行性与复核，模型负责在海量情形中完成繁重的排除工作。

有意思的是，nor 公布结果后发现，用 AI 研究同一问题的同道中人还有不少，也有网友感叹「都不知道数学领域能有这么浓厚的探索氛围」。下一步值得留意的是，这套几何约束加有限搜索的思路能否推广到更多组合几何难题，以及人类验证与机器证明之间如何形成更可靠的协作流程。