AI 辅助完成 11 正方形最优堆积形式化证明

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

68AI 研判分

核心综述

研究团队利用 AI 辅助在 Lean 证明助手中完成了 11 个正方形在单位正方形内最优堆积的完整形式化证明，并通过了包含 7920 个模块的验证。该成果确立了精确的最优边长代数表达式，但核心数值证书依赖 `native_decide`，因此信任边界扩展至 Lean 内核及原生编译器，而非纯内核验证。

报道全文原始报道全文

本文目录2 个章节

Lean 中的十一正方形装箱问题

完整的极值性证明已通过带有原生数值证书的验证。 已完成的 EvolvingPrograms 验证运行接受了全部 7,920 个本地 Lean 模块，其最终审计报告指出零项准入例外。本仓库从提交 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 不变。在装有 Python 3、Git、curl 和 tar 的 Linux 系统上：

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

在 macOS 上，请先安装 elan 启动器，然后使用相同的命令。如果已安装 elan，bootstrap 过程可以准备固定的工具链和依赖缓存。请根据机器性能选择合适的 worker 数量；模块是串行编译的。现有的有效凭证（receipts）是可复用的。添加 --fresh 参数可强制完整重放；按 Ctrl-C 可干净地停止运行器。

该命令会检查每个本地模块，并执行最终的源代码、凭证、依赖项和公理审计。最终结果中必须包含 OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、零准入（zero admissions），以及 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/ 目录中。