完整的最优性证明已通过带有原生数值证书的验证。完成的演进程序（EvolvingPrograms）验证运行接受了全部 7,920 个本地精益（Lean）模块，最终审计报告零准入。本仓库从提交 1bf942a7af1ea330e95489d8997deebd4227ca71 导入了那些确切的证明源和固定构建配置。部分昂贵的精确数值证书检查使用 native_decide，几何、检查器可靠性和证明组装保留普通 Lean 证明，因此最终定理信任 Lean 的内核和原生编译器，而非仅内核验证声明。
正文
Eleven-square packing in Lean
完整的最优性证明已通过验证，使用了原生数值证书。 已完成的 EvolvingPrograms 验证运行 接受了全部 7,920 个本地 Lean 模块，最终审计报告 零 admission。本仓库从提交 1bf942a7af1ea330e95489d8997deebd4227ca71 导入这些确切的证明源码和固定的构建配置。证据和范围见验证报告。
选定的高成本、精确数值证书检查使用 native_decide。几何、检查器可靠性和证明组装仍使用普通 Lean 证明。因此最终定理信任的是 Lean 内核和原生编译器；这不是仅内核的验证声明。已批准的数值声明及其确切的源码哈希记录在 verification/native-certificates.json。
最优边长为
[ T = \frac{6u+4}{1+2u-u^2}, ]
其中 u 是
[ 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0. ]
在 (9/25,37/100) 内的唯一根。该构造达到约 3.8770835900228141773。模型允许任意朝向、合法边界接触和不相交的开内部。ElevenSquare/Optimality.lean 中的公开声明以及完整的 T03 源码树与本仓库之前的主分支一致。
入口文件
| 文件 | 用途 |
| --- | --- |
| ElevenSquare/Foundations.lean | 几何、精确端点、达到最优的构造、闭胞覆盖及有限情形归约。 |
| ElevenSquare/Pending/ | 原始公开接口，现已由整合证明消解。目录名是历史遗留。 |
| ElevenSquare/Interop/Wand125/ | 与已并入的上游证书结果的连接。 |
| ElevenSquare/Tasks/ | 几何论证、检查器、证书数据及本地解析证明。 |
| Sqpack/ | 已并入的证书检查器、生成的证明及简化。 |
| ElevenSquare/Optimality.lean | 无条件最优性及边长下界定理。 |
| ElevenSquare/Verification.lean | 公开证明目标的公理查询。 |
复现验证
项目固定 Lean 4.34.1 和 Mathlib 修订版 d13f23b723b8a846827a245b89c10fc7d3f11612。保持 lake-manifest.json 不变。在 Linux 上需 Python 3、Git、curl 和 tar：
bash scripts/run_verification.sh --bootstrap --jobs 2
在 macOS 上，先安装 elan 启动器，然后使用同样的命令。若已安装 elan，bootstrap 会准备固定的工具链和依赖缓存。根据机器选择合适的工作线程数；模块串行编译。已有的有效 receipt 可复用。加 --fresh 强制完整重放；Ctrl-C 可干净地停止运行器。
该命令检查每个本地模块，并执行最终的源码、receipt、依赖和公理审计。最终结果需包含 OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、零 admission，以及 trust_model: lean_kernel_and_native_compiler。仅达到 100% 已编译模块是不够的。
仅源码检查（不需要 Lean）：
python3 scripts/check_sources.py
手动工作流与 Ubuntu 说明 也支持可恢复的验证。推送不会启动工作流。成功的源码运行使用了 EvolvingPrograms 更大的 runner；它并不确立冷构建时间或 2–3 小时的 macOS 保证。
不要在此快照上运行历史物化命令或 verify.py --setup：它们会恢复已被取代的生成源码。构建对象和日志应放在被忽略的 .lake/ 和 .verification/ 目录中。
致谢与来源
感谢 EvolvingPrograms、@ctjlewis 以及所有项目贡献者 在形式化和验证方面的工作。个人及上游致谢见 ACKNOWLEDGEMENTS.md，源码历史见 PROVENANCE.md，保留的声明见 integrations/wand125。历史简化笔记和部分审计记录已保留；其旧的未完成状态陈述已被完成运行报告取代。
评论
讨论集中在正方形填装证明的可行性与文档呈现上，少数人认为堆叠即可无需证明，少数人惊讶能证最优并视人工智能为民主化工具，较多人抱怨原项目缺图缺说明。
认为问题显然无需证明
- 认为直接将方块相邻堆叠或无限薄片叠加即可，质疑证明的必要性（少数人） > 这不明摆着吗，直接把方块挨着堆就行，难道我漏了什么？（@rfgplk）
对能证明最优性感到惊讶
- 未料到这个看似繁琐优美的填装问题能被严格证明最优（少数人） > 真没想到有人能证明那个又烦人又漂亮的东西的最优性。（@kevinwang）
认为人工智能带来证明民主化而非取代数学家
- 指出基础方法如不可避免集和线性规划早已存在，人工智能仅降低工作量使业余爱好者能完成形式化验证，并非超人类窃取成果（少数人） > 人工智能做的不是取代数学家，而是让喜欢填装的业余者也能完成并验证证明，这是民主化。（@DevelopingElk）
认为原项目文档与图示不足
- 项目 README 缺少图示与简短问题说明，但社区主动补充了外部图片资源（较多人） > 项目首页要是能有简短问题说明就好了（@ur-whale）
有价值的补充
- 有从业者分享曾用区间算术分支定界处理类似问题，正确设置舍入模式耗费数周，侧面印证计算复杂性。
- 回忆 David Huffman 的课程提及球填装在 11 维外均极困难，反映高维填装的历史认知。
- 解释正方形填装定义：将单位正方形塞入边长非整数的大正方形时，如何最大化数量成为非平凡问题。
- 有人指出该填装图形并非任意丑陋，其结构有深层原因，并指向外部图解。
- 社区提供了专门收录正方形填装的站点、三角形视角视频及关联问题视频等丰富可视化资料。