11 个正方形怎么摆最省：一份能被机器复查的证明

把 11 个同样大的正方形塞进一个尽量小的正方形里，最省能省到什么程度？这个问题看上去像拼图游戏，验证起来却要用到 Lean 和一台高性能计算集群。

一、发生了什么

GitHub 上的 11SquaresFormalized 仓库，标题写的是「11 个正方形装箱最优性证明的 Lean 形式化」。它声称给出了无条件最优性：11 个单位正方形装进一个大正方形，大正方形的最小边长是

T =（6u+4）/（1+2u−u²）

其中 u 是区间（9/25, 37/100）内唯一满足一个八次多项式的根。按仓库给出的数值，T 约等于 3.8770835900228141773。

证明覆盖的设定是：小正方形可以任意朝向，允许合法的边界接触，只要求内部互不重叠。这比「只许平放」的版本难得多。

仓库用的是 Lean 4.34.1 和指定版本的 Mathlib，全部 7920 个本地模块通过检查，最终审计记录为零个 admission。验证工作在一台 HPC 集群上完成，贡献者名单里有一位专门负责让证明能在集群上跑起来。

有一点必须说清楚：仓库没有写用了哪个 AI 模型。「AI 辅助」的说法来自外部转述，代码和文档里找不到对应的模型、提示词或生成记录。原始证明来自另一个仓库 EvolvingPrograms/11SquaresEvolving，这个仓库做的是整合、固定版本和重新验证。

做形式化的人。 这是一个可复现的工程样本：固定工具链、固定依赖、把昂贵的数值检查交给原生证书、把几何和检查器的可靠性留在普通 Lean 证明里。

研究离散几何的人。 任意朝向的装箱问题一直是硬骨头。这个结果如果站得住，方法和结论都值得读。

关心 AI 做数学的人。 这件事的价值不在「AI 又解了一题」，而在「AI 生成的东西能不能被机器验收」。后者才是可规模化的部分。

先跑源码检查。 仓库带 scripts/check_sources.py，不需要装 Lean，先确认源码哈希和声明的证书对得上。
再跑完整验证。 仓库自带一个验证脚本，Linux 上直接跑，带 bootstrap 参数，并行数按机器核数自己调；macOS 要先装 elan。第一次会拉一堆依赖，耗时较长。
看三个标记。 编译全部模块还不够，输出里必须出现「最优性已由原生证书证明」那一行、zero admissions，以及信任模型声明。
读信任边界。 仓库明确写的是「Lean 内核加原生编译器」，不是纯内核验证。也就是说，最终结论还依赖编译器正确性。这一点决定了你该有多信它。

「机器验证过，就是绝对正确。」 形式化把错误从「证明写错」转移到「规格写错」和「工具链可信」。如果命题的建模不对，证出来的东西和你想的不是一回事。仓库把这一点写在文档里，值得读。

「AI 独立完成了这个证明。」 仓库署名是一组贡献者，工作包括整合、修复、在集群上执行验证。AI 是否参与、参与到哪一步，公开材料没有交代。把它写成「AI 解决」，是替作者说了他们没说的话。

「11 个正方形太小，没什么意义。」 小问题的价值在方法：它把「几何论证 + 数值证书 + 机器检查」这条流水线跑通了。流水线能复用，单个结论不能。

这份仓库真正提供的不是一个新的装箱数字，而是一条可复现的验收路径；在 AI 能批量产出证明的时代，能验收比能生成更稀缺。

功能与价格以官方公告为准。本文写于 2026 年 10 月 18 日。