鱼羊 发自 凹非寺 量子位 | 公众号 QbitAI
AI 现在真是开启数学证明扫荡模式了。
刚刚，又有数学爱好者用 GPT-6 Astra 把一个 57 年数学难题推进了一大步。
给你 N 个半径为 1 的圆盘，怎么把它们塞进一个大圆里，才能让大圆的半径尽可能小？
于是这一次，数学爱好者 nor 掏出了 GPT-6 Astra ……然后一口气把 15、16、17、18 和 20 这 5 种情况，也就是 N ≤ 20 的剩余情况都给严格证明了……
此前，只有 N ≤ 14 和 N=19 的情况已经得到验证。
啊对了，N 到 20，并不是 AI 的极限，只是 nor 没想着往下证了……
咱们先把这个问题用更数学的形式来归置归置。
假设有 N 个半径均为 1 的圆盘，以及一个半径为 R 的大圆。
要求：
所有小圆盘必须完全位于大圆内部，可以与大圆边界相切，但不能超出边界。
任意两个小圆盘不能发生内部重叠，但允许彼此相切。
小圆盘可以在大圆内任意移动、排列，不限制排列方式。
问题是：对于给定的正整数 N，大圆半径 R 最小可以是多少？
看上去是一道平平无奇奥数题，但实际上，寻找最优排列只是问题的第一层，但就难在如何严格在数学上证明，排列已经达到极限，没有其他更好的摆法。
在 1968 年，美国数学家葛立恒就证明了 N ≤ 7 的情况。
1969 年，数学研究者 Udo Pirl 把证明范围推进到 10 个圆盘，并进一步研究了 11-19 个圆盘的排列方案。
但一直到 2003 年前后，N ≤ 14 以及 N=19 的情形才被严格证明。
他本人在十多年前就关注到了这个题目，而这个问题在过去十几年间确实也没啥进展……
那还说啥，丢给 GPT-6 Astra 正好（bushi）。
nor 也循序渐进的：先让 GPT-6 Astra 处理 N=15 的情况；模型解决之后，再让它把同样的方法推广到 16、17，以及 18 和 20 …… GPT-6 Astra 都成功给出了证明结果。
只是嘛……
证明过程一如既往晦涩难懂，令人费解。
不再直接寻找最优解，而是通过几何约束，把无限多种可能的排列缩减为有限的情况，再用计算机逐一排除，最终严格证明经典排列已经最优。
把靠外的圆盘推向边界。证明在满足特定条件时，可以把靠近外圆的圆盘向外移动，而不会引起重叠。这样就把圆盘分成了边界上的一组和内部的一组。
利用角度关系排除大量排列。因为圆盘不能重叠，它们之间必须保持一定的角度间隔。如果某种排列要求的角度总和超过 360 °，就可以直接排除。
让计算机枚举剩余可能。不再搜索每个圆盘的具体坐标，而是检查圆盘到圆心的距离区间及其环绕次序。
用几何刚性证明精确最优。前面的搜索只能证明，所有可行排列都非常接近已知的经典排列。接下来利用圆盘之间的接触约束，证明这些排列无法发生符合条件的微小变形，从而把 " 非常接近 " 提升为 " 严格一致 "。15 个圆盘的情况使用了另一种奇数环论证。
还原原始排列。最后证明，原始排列中必然至少有一个圆盘接触外圆边界。这意味着不可能把所有圆盘塞进半径更小的外圆，从而完成最优性证明。
值得强调的是，并不是 nor 给了一轮提示词，Astra 就哐哐哐全给证完了。
nor 在博客文章中写道，他作为人类，在这项工作种的贡献包括：
确定问题的可行性、引导模型、与漏洞百出的网页用户界面作斗争、忍受糟糕的文案、修复细微问题、反复推敲阐述、手动验证其有效性，以及使用 Astra 和 Opus 5.5 重新检查所有内容。
One More Thing
挺有意思的一件事是，nor 把结果一发出来，发现用 AI 在研究同一个问题的同道中人还不少。
原文链接： [ 1 ] https://nor-blog.pages.dev/posts/2026-10-11-circle-in-circle-packing-15-20/ [ 2 ] https://x.com/norxornor/status/2109078411251454017
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
