11 个正方形最优堆叠问题在 Lean 中完成机器验证证明
一个名为 11SquaresFormalized 的 GitHub 项目发布了 11 个正方形最优堆叠的完整最优性证明，已通过 Lean 验证。验证运行接受了全部 7,920 个本地 Lean 模块，最终审计报告零 admission。最优边长约为 3.8770835900228141773，由公式 T=(6u+4)/(1+2u-u²) 给出，其中 u 是某八次方程在 (9/25, 37/100) 内的唯一根。部分精确数值证书检查使用 native_decide，因此最终定理信任 Lean 内核与原生编译器，而非仅…
推荐理由可复现的 Lean 4 形式化证明，含 7,920 模块验证脚本与固定工具链