# 11 个正方形最优装箱问题的 AI 辅助证明

- 原标题：AI-assisted proof of optimal packing for 11 squares
- 类型：项目
- 来源：GitHub
- 发布时间：2026-09-30
- 首次精选：2026-10-26 16:27
- 分级：值得看
- 学习层级：深入
- 主题：[ai-mathematics-proofs](<https://oplearnx.com/md/topics/ai-mathematics-proofs.md>)（第 16 位）
- 原文链接：[https://github.com/Queuingtheorydotcom/11SquaresFormalized](<https://github.com/Queuingtheorydotcom/11SquaresFormalized>)
- 本站页面：[https://oplearnx.com/resources/pk\_7690aa2f58c4](<https://oplearnx.com/resources/pk_7690aa2f58c4>)

## 摘要

一个 GitHub 仓库，包含 11 个正方形装箱最优性证明的 Lean 形式化版本。据 README，完整证明已在 EvolvingPrograms 的验证运行中通过，涉及 7,920 个本地 Lean 模块，最终审计报告零处 admitted；部分精确数值证书检查使用 native\_decide，几何、检查器可靠性与证明组装仍用普通 Lean 证明。最优边长由含八次方程根 u 的公式给出，数值约为 3.8770835900228141773，并附有验证报告与证书哈希记录文件。

## 热度

- 档位：热度强
- 7 天新增 star：0
- 30 天新增 star：+27
- Hacker News：[119 分 · 55 条评论](<https://news.ycombinator.com/item?id=49993121>)
- 社区讨论：1 帖

## 项目信息

- 语言：Lean
- 许可：未声明
- 最近提交：2026-10-06
- Star：28
- Fork：1

## 上手方式

```sh
bash scripts/run_verification.sh --bootstrap --jobs 2
```

摘自 [README](<https://github.com/Queuingtheorydotcom/11SquaresFormalized/blob/main/README.md>)

---
来源：LearnMap · 学径（https://oplearnx.com）