AI助攻17方块装箱问题获首个完整Lean形式化证明

围绕 1998 年 Bidwell 提出的 17 个单位正方形装箱问题，Marc Leonard Overbeck 借助 Codex 与 Claude 产出一个候选证明，声称 s(17)=4.6755300 即 Bidwell 的装箱方案已是最优解。随后 Oscar Fitzhardinge 发布了该最优性的首个完整 Lean 形式化证明，确认 17 个单位方块无法装入更小的正方形。

2026-10-13 ~ 2026-10-14 · 2 条相关

• 用 Codex 与 Claude 求解 17 正方形装箱证明，s(17)=4.6755 — ctjlewis · 2026-10-13
• AI 助攻数学：Bidwell 17 方块装箱最优性获首个完整 Lean 证明 — tak3sh8 · 2026-10-14