19 个单位方块最优装箱问题有了 Lean 形式化证明
ctjlewis · x · 2026-10-16
开发者 ofitzharding 在 GitHub 开源了 sq19 项目，用 Lean 定理证明器形式化了经典的 19 个单位方块装箱问题：当且仅当容器边长 L ≥ 3 + 4√2/3 ≈ 4.885618 时，19 个单位方块可装入（允许任意旋转与接触）。
- 证明核心定理为 Sq19.square19optimality，给出装箱可行性与该下界的等价关系
- 依赖公理仅 propext、Classical.choice、Quot.sound，另加 4,320 个 nativedecide 证书检查，信任 Lean 编译器与原生求值器
- 定理导入闭包共 13,143 个模块，仓库采用 MIT 许可证
这是用形式化方法攻克组合几何最优性证明的一个小而精的案例。
「研究」频道最新
- Lean v4.35.0 自带四个已验证内核，其中之一由 Claude 写成并自证一致 — geoffreyirving · 2026-10-16
- MP-Bench：语音 Agent 群聊插话判断仅与抛硬币相当 — solyarisoftware · 2026-10-16
- 对 Qwen3-8B 做神经元级 GWAS+PheWAS，定位安全相关神经元 — Sauers_ · 2026-10-16
- 770B 参数压进 214GiB：腾讯混元量化团队拆解 Hy4 Preview 压缩术 — coolmum18 · 2026-10-16
- 200 局国际象棋实测：作者认为上下文学习目前并不奏效 — akbirthko · 2026-10-16
- LARK-Lab 提出 Mosaic：跨会话的 Agentic 强化学习新范式 — LARK-Lab · 2026-10-16