n=11 方形装箱最优性获形式化证明
square packing 项目宣布经典组合几何难题「11 个单位正方形装入最小正方形」的最优性获得证明，并通过机器校验的证明 T-060 确认 Trump 1979 年提出的布局是最优解，最优边长 s(11)=3.87708359…。证明借助 Astra 与 Claude 在 Lean 证明助手中完成形式化验证。这一成果是 AI 辅助数学研究的又一实际进展，值得关注。
已确认
- 最优值 s(11)=3.87708359…，对应 Trump 1979 年的布局，经机器校验证明 T-060 确认为最优
- 形式化验证在 Lean 中完成，使用了证明助手 Astra 与 Claude
- ctjlewis 在项目中承担编译 Lean 证明、教团队使用 GitHub Actions runner 的工作；其组织提供 64 核托管 runner 加速流程，仅编译 Lean 即花费 300 美元
- 据 ctjlewis 转述，The Squares Project 由 Joshua Levy 于 2026 年 8 月发起，展示方格装箱问题在 AI 辅助研究下的进展：获得 n=11、17-20 等低值的新下界；Kleddamag 得到 31/8 的认证下界
- 项目产出系列论文
为什么重要
- 「cursed」的 n=11 构型长期以来被视为难解的几何装箱问题，其最优性证明连同形式化验证是组合几何领域的实质性进展
- 整个流程展示了 AI（Astra、Claude）与人类数学家协作完成并验证非平凡数学证明的可行路径，成本可控（编译仅 300 美元）、基础设施（GitHub Actions runner）易复用
2026-10-07 ~ 2026-10-07 · 5 条相关
一手来源
- AI 协作证明攻克 11 方块装箱难题,Trump 1979 年布局被证明最优 — ctjlewis ·
- 11 个正方形装箱最优性获证明：Astra 与 Claude 协助在 Lean 中形式化 — ctjlewis ·
- AI 驱动方格装箱研究爆发:53 格最优装箱刷新,11 格问题获最优性证明 — ctjlewis ·
- 【源头】11 个正方形装箱最优性获证明：Astra 与 Claude 协助在 Lean 中形式化 — ctjlewis · 2026-10-07
- AI 数学 proof 项目编译 Lean 花 300 美元,64 核 GitHub runner 加速 — ctjlewis · 2026-10-07
- 【源头】AI 驱动方格装箱研究爆发:53 格最优装箱刷新,11 格问题获最优性证明 — ctjlewis · 2026-10-07
- 数学家团队形式化验证:n=11 方形装箱问题确为最优解 — ctjlewis · 2026-10-07
- 【源头】AI 协作证明攻克 11 方块装箱难题,Trump 1979 年布局被证明最优 — ctjlewis · 2026-10-07