AI 辅助完成 11 个正方形最优装箱问题的 Lean 形式化证明

开源项目 11SquaresFormalized 宣布通过 Lean 完成了 11 个正方形最优装箱问题的完整数学证明，所有 7,920 个本地 Lean 模块均已通过验证且无未证假设。该证明计算出正方形最优边长约为 3.87708359，信任模型基于 Lean 内核与本地编译器，支持在固定版本 Lean 4.34.1 环境下完整复现。