11 个正方形装箱最优性获证明：Astra 与 Claude 协助在 Lean 中形式化
ctjlewis · x · 2026-10-07
11 个正方形装箱问题（在单位正方形内装入 11 个小正方形的最大边长）的最优性被证明，并借助证明助手 Astra 与 Claude 在 Lean 中完成形式化验证。
- 最优值 s(11) = 3.87708359…，对应的 packing 由 Walter Trump 于 1979 年手工构造；
- 证明（T-060）由 Queuingtheorydotcom 2026 年给出，采用计数论证加几何排除、精确对称性与局部捕获等论证，斜率涉及一个 8 次多项式的根；
- 独立核查方（Squares Project 案例记录页）重放了源输入并组合了精确义务，确认结果成立，尽管公开发布的缓存审计中有四个过期的终态摘要，需绕过 RUNALL 路线独立验证；
- 这是 AI 辅助数学研究（LLM + 形式化证明）落地的又一标志性案例。
所属事件:11 个正方形装箱问题最优性获 Lean 形式化证明(2 条相关)→
「研究」频道最新
- 研究发现:选对开头 token,base 模型推理可媲美 RL 训练效果 — RulinShao · 2026-10-07
- AI 数学证明走向开源式协作:方格装箱证明附可视化讲解 — ctjlewis · 2026-10-07
- 开源平台 Overmind：用生产轨迹持续训练与改进 AI Agent — cneuralnetwork · 2026-10-07
- 仅凭 top-20 logits 约 100 次查询即可恢复未询问属性 — sineadwilliamso · 2026-10-07
- 研究发现：top-k logits 泄露的信息量与 tuned lens 相当 — sineadwilliamso · 2026-10-07
- AutoAWQ 作者：约 4.3 万美元和一个 B300 节点四周可复现 Bonsai 2 — airesearch12 · 2026-10-07