把一把硬币塞进圆盒，摆出一种看起来很紧的方案并不算完。真正困难的是证明：无论怎样挪动，都不可能换一个更小的盒子。数学爱好者 nor 借助 GPT-6 Astra，尝试为 15、16、17、18 和 20 个等大圆盘的经典摆法补上这一步。据量子位转述，这五种情形此前一直缺少严格的最优性证明；若结果经独立核验，意味着 的空缺将被补齐。
难的不是摆出来，而是排除其他摆法
这类问题叫“圆盘装圆”：把 个半径为 1、互不重叠的小圆盘放进一个半径为 的大圆，并让 尽可能小。
人们很早就找到了漂亮的候选排列。Erich's Packing Center 的资料显示，15 和 18 圆的方案可追溯至 Kravitz 在 1967 年的构造，16 和 20 圆来自 Goldberg 1971 年的工作，17 圆方案由 Reis 在 1975 年给出。它们像五把早已配好的钥匙，缺的是证明没有另一把更好用的钥匙。
这也解释了“57年难题”的说法：Udo Pirl 在 1969 年研究过 11—19 个圆盘的排列，此后相关证明长期没有补齐。但这个标签不能笼统覆盖全部五种情形，尤其 并不在 Pirl 当年的 11—19 范围内。
先把无限可能压成有限清单
据量子位转述，证明的关键不是继续搜索更漂亮的坐标，而是利用几何约束，把连续、无限的排列空间缩成有限情形。
第一步是把部分靠外的圆盘推到大圆边界，并证明这一移动不会造成重叠。接着利用圆盘间必须保持的角度间隔，排除那些绕一圈会超过 的组合。剩余情况交给计算机枚举，但计算机检查的不是每个圆盘的精确坐标，而是它们到圆心的距离区间和环绕次序。
枚举只能说明可行排列非常接近经典方案，还不能自动得到“完全相同”。最后一段论证依靠接触约束和几何刚性——也就是圆盘彼此顶住后，不能再做满足条件的微小变形——把“几乎如此”推进到严格最优。 没有照搬同一条路线，而是使用了不同的“奇数环”论证。
这次进展为什么值得看
我们此前讨论过，模型生成数学手稿、形式化检查和同行认可不是一回事。这次更值得注意的，是任务从集中解题走向了一个有历史、有旧候选答案、也有明确证明缺口的研究问题。
它也不是模型独立完成的成果。nor 称，自己负责判断问题是否可做、引导模型、修复细节、反复打磨论述和人工验证，并用 Astra 与 Opus 5.5 复核全部内容。更准确的描述是人机协作证明：人选择问题、控制方向并检查结论，模型帮助寻找和补全论证。
局限与未知
- 目前材料只有量子位的一篇二手报道。“严格证明”和“补齐 ”均来自 nor 的自述及媒体转述，尚无独立数学专家评审、同行评议论文或可复现核验材料。
- GPT-6 Astra 的具体版本、公开状态，以及模型与人工各自贡献到哪一步，现有材料没有充分说明。
- 因此，这更适合被视为一项值得核验的人机协作研究进展，而不是已经获得数学共同体确认的最终定论。