AI 辅助证明 11 个正方形的最优排列
AI-assisted proof of optimal packing for 11 squares
一个名为 11SquaresFormalized 的 GitHub 项目，利用 Lean 形式化验证系统，成功完成了关于 11 个正方形最优排列问题的完整证明。该项目通过 EvolvingPrograms 的验证流程，接受了全部 7920 个本地 Lean 模块，最终审计报告为零误报。证明过程结合了 Lean 的几何推理与原生数值证书（native numerical certificates），确保了结论的绝对可靠性。最优边长被精确计算为约 3.877，该模型允许任意方向旋转和合法边界接触。这一成就标志着数学证明与 AI 辅助验证技术的深度融合，为复杂几何问题的形式化验证树立了新标杆。
完整的优化性证明已通过原生数值证书的验证，最终审计报告显示零误报。
HN 评论区
46- dkural
乍一看，这似乎有些随意甚至丑陋，但事实并非如此——请看这里的图片和解释：https://x.com/davidmbudden/status/2107646435659481548
- yzydserd
顺便一提，正方形内嵌正方形排布问题的首选网站是：https://kingbird.myphotos.cc/packing/squares_in_squares.html
三角视图最有趣。关于这个视图还有一个 20 分钟的视频：
- DevelopingElk
我正在尝试复现该证明，并加入了一些个人改动。基本方法采用的是标准的计算机辅助“不可避免集”（unavoidable set）方法。首先，选择一些足够小的区域，使得两个正方形的中心无法同时落入同一区域，文中使用了 16 个区域。每个区域要么包含一个正方形，要么不包含，即 16 选 11 的组合，约 2000 种情况。针对每种情况，尝试将其排除。方法是识别出必须由某个正方形覆盖的区域，并传播这一信息。此外，还可以利用 Stromquist 在 1989 年使用的排布线性规划（packing LPs）来排除更多构型。随后，聚焦于剩余情况并对它们进行更细的划分。
我认为，在 AI 出现之前这项工作未被完成，唯一的原因在于它并未成为严肃的研究焦点。1989 年的计算机性能太弱，无法处理所有情况。但所有基本要素在开普勒猜想（Kepler conjecture）的证明中都已具备。AI 的作用是将所需工作量降低到足以让那些仅仅因为喜欢正方形排布问题的业余爱好者也能完成并形式化验证此类证明的程度。我自认就是这样的业余爱好者之一。因此，这并非 AI 窃取数学家证明或完成超人类任务的案例，而是民主化的体现。我确实担忧 AI 对数学领域的影响以及 AI 公司的行为，但本案并非令人担忧的实例。证明该排布最优所需的计算量将永远大到无法通过手工核查。不过，我希望能制作出关于排布线性规划或核心重叠（core overlap）的精美可视化 […]
- WithinReason
许多正方形排布的列表及图片：
- yboris
开个玩笑的版本：https://x.com/bookazoid_/status/2107771851229610331/photo/1
一个采用 11 个正方形排布设计的键盘