GitHub 仓库 11SquaresFormalized 称，11 个正方形装箱的完整最优性证明已通过验证，并带有原生数值证书。据仓库说明，EvolvingPrograms 的验证运行接受了全部 7,920 个本地 Lean 模块，最终审计报告零个 admission（未证明假设）。仓库同时给出最优边长的闭式表达，并写明最终定理信任 Lean 内核与原生编译器，而不是只依赖内核。
仓库给出的最优边长为 T = (6u+4)/(1+2u−u²)。其中 u 是八次多项式 5u⁸−10u⁷−2u⁶+14u⁵+12u⁴−6u³+2u²+2u−1=0 在区间 (9/25, 37/100) 内的唯一根。仓库称，相应构造达到的边长约为 3.8770835900228141773。
模型允许任意旋转方向、合法的边界接触，以及互不相交的开内部。无条件最优性与边长下界定理写在 ElevenSquare/Optimality.lean。仓库说明，这些公开陈述以及完整的 T03 源码树，与本仓库此前的 main 分支相比没有改动。
仓库称，完整最优性证明已通过带原生数值证书的验证。EvolvingPrograms 的验证运行接受了全部 7,920 个本地 Lean 模块，最终审计为零个 admission。本仓库从提交 1bf942a7af1ea330e95489d8997deebd4227ca71 导入这些证明源码和固定的构建配置。证据与范围写在 docs/VERIFICATION_20261006.md。
部分开销很大的精确数值证书检查使用了 native_decide。几何论证、检查器的正确性以及证明组装仍是常规 Lean 证明。因此，发布方写明，最终定理信任 Lean 内核和原生编译器，这不是仅依赖内核的验证。获准的数值声明及其精确源码哈希记录在 verification/native-certificates.json。
复现说明要求，最终结果须出现 OPTIMALITY_PROVED_WITH_NATIVE_CERTIFICATES、零个 admission，以及 trust_model: lean_kernel_and_native_compiler。仓库称，仅仅编译完 100% 的模块并不足够。
项目固定使用 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 启动器，再执行同一命令。该命令会检查每一个本地模块，并做最终的源码、回执、依赖与公理审计。不启动 Lean 的源码检查为 python3 scripts/check_sources.py。
仓库说明，向仓库推送不会自动启动工作流。已成功的那次源码运行使用的是 EvolvingPrograms 更大的运行器；这次运行并不确立冷构建所需时间，也不构成在 macOS 上 2 至 3 小时可以跑完的保证。
仓库致谢 EvolvingPrograms、@ctjlewis 以及所有项目贡献者所做的形式化与验证工作，并另指向 ACKNOWLEDGEMENTS.md、PROVENANCE.md 与 integrations/wand125。来源原文没有说明人工智能具体参与了哪些环节。
