AI 辅助证明 11 个正方形最优装箱通过验证
AI 总结
一个 GitHub 仓库发布消息称，11 个正方形最优装箱问题的完整最优性证明已在 Lean 中通过验证：EvolvingPrograms 的验证运行接受了全部 7,920 个本地 Lean 模块，最终审计报告“零 admission”。该仓库固定使用 Lean 4.34.1 与指定 Mathlib 修订版，最优边长由公式 T=(6u+4)/(1+2u−u²) 给出（u 为某八次方程在 (9/25,37/100) 内的唯一根），构造值约为 3.8770835900228141773。部分昂贵且精确的数值证书检查使用了 native_decide，因此最终定理信赖的是 Lean 内核加上原生编译器，而非仅内核验证。
深度见解
这是 AI 辅助形式化数学的一个具体案例：把长期开放的最优装箱问题完整搬进 Lean，并以可复现的脚本和证书审计公开验证过程。