Lean 验证 11 个正方形最优排列：形式化证明锁定 3.877 边长

一句话看懂：2026 年 10 月 7 日前后，一个开源项目宣布在 Lean 4 中完成 11 个正方形最优排列的形式化验证，并给出最优边长约 3.877083590022814。它值得关注，是因为这是 AI 辅助定理证明工具在经典几何优化问题上的一次完整验证落地。

事件核心：发生了什么

项目 11SquaresFormalized 将 11 个正方形的最优排列证明完整形式化到 Lean 4 中，并已通过验证。根据公开材料，验证运行接受了全部 7,920 个本地 Lean 模块，最终审计报告显示 zero admissions（零未证明假设）。该仓库导入自提交 1bf942a7af1ea330e95489d8997deebd4227ca71 的证明源码和锁定构建配置。

关键数据方面，最优边长 3.8770835900228141773，由公式 T = (6u+4)/(1+2u-u^2) 给出，其中 u 是区间 (9/25, 37/100) 内方程 5u^8-10u^7-2u^6+14u^5+12u^4-6u^3+2u^2+2u-1=0 的唯一根。模型允许任意朝向、合法边界接触和互不相交的内部。项目固定使用 Lean 4.34.1 和 Mathlib 修订版 d13f23b723b8a846827a245b89c10fc7d3f11612。

技术实现上，部分昂贵的精确数值证书检查使用了 native_decide，而几何、检查器可靠性和证明组装仍保留普通 Lean 证明。因此最终定理信任的是 Lean 内核和原生编译器，并非仅内核验证。已批准的数值声明及其精确源哈希记录在 verification/native-certificates.json 中。

为什么重要

这首先是一个方法层面的样本：它展示了大模型时代 AI 辅助证明工具链（Lean、Mathlib、EvolvingPrograms 等）已经可以支撑相对复杂的几何优化定理的端到端形式化验证。与常见的“AI 生成证明摘要”不同，这里要求每个模块编译通过、审计零放行，且可复现验证流程。

其次，它把经典打包问题从“近似最优构造”推进到“无条件最优性定理”。对于形式化数学社区，这意味着数值证书与符号证明的混合路线可以走通；对于 AI 行业，它提供了一个可复用的验证范式——当模型生成的数学内容需要可信落地时，内核级检查仍然是最硬的一道门槛。

不过目前公开信息显示，该验证依赖原生编译器信任假设，且成功运行使用了 EvolvingPrograms 的较大运行器，并未确立冷构建耗时或 macOS 上 2 至 3 小时的保证。它是一次完整验证，但不是“仅内核验证”的声明。

对用户/开发者/创作者的影响

对开发者和形式化数学研究者来说，这个仓库给出了可复现的入口：运行 bash scripts/run_verification.sh –bootstrap –jobs 2 可检查所有本地模块并执行最终审计；要求达到 OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、零 admissions 和 trust_model: lean_kernel_and_native_compiler。纯源码检查可用 python3 scripts/check_sources.py。对 AI 工具开发者而言，它说明将大模型用于数学推理时，可以把“生成候选证明”和“Lean 内核实证检查”分层，前者提高探索效率，后者守住可信边界。对普通用户，这类工作暂时不会带来直接产品变化，但它可能逐步影响未来 AI 数学助手、教育工具和自动验证服务的可靠性标准。