# 11 个正方形最优装箱的 AI 辅助 Lean 证明通过验证

> 原标题：AI-assisted proof of optimal packing for 11 squares

- 来源：Hacker News 首页
- 发布时间：2026-10-07T14:10:55.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/jjcyooob6jr69clj4nea0r5zd
- 原文：https://github.com/Queuingtheorydotcom/11SquaresFormalized

## 摘要

11 个正方形装箱问题的最优性证明在 Lean 中完成验证，EvolvingPrograms 的验证运行接受了全部 7,920 个本地 Lean 模块，最终审计零 admission。该证明给出最优边长公式，构造值约为 3.8770835900228141773，项目固定 Lean 4.34.1 与指定 Mathlib 版本，可复现验证。