11 正方形最优装箱 Lean 形式化：仓库新增 Pending 入口与哈希记录细节
2026.10.07 · 事件 · 开源验证 · 开源项目
仓库补充 Pending 入口、证书哈希文件与 macOS 复现前置等细节。
11 个正方形装箱最优性已在 Lean 中形式化，完整证明通过 native numerical certificates 验证，EvolvingPrograms 运行接受全部 7,920 个本地 Lean 模块且零 admission。GitHub 仓库公开从 commit 1bf942a7 导入的证明源码与固定构建配置，并新增 Pending 入口、native-certificates.json 哈希记录…
- 新增 ElevenSquare/Pending/ 入口，原公开接口已由整合证明解
- 已批准数值声明及精确源码哈希记录在 verification/native-ce
- 要求 lake-manifest.json 保持不变，macOS 需先装 ela
- 仅 100% 模块编译不充分，仍需通过最终审计
- 禁止运行历史物化命令或 verify.py --setup
为什么值得看
仓库公开可复现验证细节，让形式化结论可被机器复核与审计。
适合谁关注
Queuingtheorydotcom 仓库与 EvolvingPrograms 等贡献者