AI 助攻数学：Bidwell 17 方块装箱最优性获首个完整 Lean 证明
tak3sh8 · x · 2026-10-14
Oscar Fitzhardinge 发布了 Bidwell 1998 年 17 方块装箱问题最优性的首个完整 Lean 形式化证明，确认 17 个方块无法装入更小的正方形（s(17) = 4.67553009...）。
该证明借助 OpenAI 的 Astra 与 Anthropic 的 Opus 5.5 协作完成，代码开源在 GitHub（ofitzharding/sq17-lean），并致谢了 Manasseh 与 ojoshe 的前期工作。这是 AI 辅助形式化数学的又一案例：把长期只有数值证据的装箱结果变成机器可验证的定理。
所属事件:AI助攻17方块装箱问题获首个完整Lean形式化证明(2 条相关)→
「研究」频道最新
- 潜艇网络战研究发现：操作员认知容量随战况剧烈波动 — J_MaestreVidal · 2026-10-14
- Recova 用编码智能体在仿真中练出机器人自恢复能力，人工干预率从 87.5% 降到 0% — Lianhuiq · 2026-10-14
- NVIDIA AlphaNIST：纯二值奖励让机器人自悟装配技能，成功率 98.2% — abhishekunique7 · 2026-10-14
- 加密思维链可被还原：三大厂商推理轨迹窃取攻击公开 — matthew_d_green · 2026-10-14
- 多数人脑中存有来自母亲的细胞，八旬老人也不例外 — AnnaCiaunica · 2026-10-14
- 循环层让小模型决策准确率大增：1.4B 逼近 3 倍大模型 — rohanpaul_ai · 2026-10-14