人工智能辅助证明11个方块的最佳填充

完整的优化证明已经通过本地数值验证。完成的EvolvingPrograms验证过程成功通过了所有7,920个局部Lean模块的检查，而其最终审计报告显示没有任何错误。

该仓库直接使用了在commit 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目录中的公开声明以及完整的T03源代码树与这个仓库之前的主分支保持一致。

该项目使用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启动器，然后使用相同的命令。的引导程序可以在启动时准备固定的工具链和依赖项缓存是已经安装。选择适合机器的工人人数;

模块是连续编译的。现有的有效收据是可重复使用的。添加--新鲜到强制完整重播;Ctrl-C干净地阻止跑步者。该命令检查每个本地模块并执行最终的源、接收、依赖性和公理审计。

要求OPTIMALITY_PROVED_BY_NATIVE_CERTIFICATES,零准入和信任模型：lean_core_and_native_compiler在决赛中结果.仅达到100%的已编译模块是不够的。

不含Lean的纯源代码检查是：python3脚本/check_source。py手动工作流程和Ubuntu说明还支持可验证。按下不会启动工作流程。成功的源代码运行使用了EvolvingPrograms的更大的runner;

它没有建立冷构建运行时或2-3小时的macOS保证。请勿运行历史物化命令或验证。py --设置on this快照：它们恢复被取代的生成源。生成对象和日志属于被忽视的。

湖/和.验证/的目录我们感谢EvolvingPrograms、@ctjlewis和每一位项目贡献者所做的形式化和验证工作。请参阅确认。个人和上游信贷的MD，起源。MD表示源历史记录，Integrations/wand 125表示保留通知。

历史简化注释和部分审计记录被保留;它们旧的未完成状态陈述被完整运行的报告取代。