Hacker News AIT2·68 分
AI 辅助完成 11 正方形最优堆积形式化证明
原文标题：AI-assisted proof of optimal packing for 11 squares
- AI 辅助生成的 Lean 证明通过 7920 个模块验证，零拒绝，解决了 11 正方形堆积这一长期未决的几何优化问题。
- 给出了最优堆积边长的精确代数解（基于八次多项式的唯一根），超越了以往的近似数值结果。
- 关键数值检查使用 `native_decide`，意味着最终定理的信任依赖于 Lean 内核和原生编译器，而非纯粹的逻辑内核验证。