11 方块装箱问题用 40 万行 Lean 代码完成形式化
ctjlewis · x · 2026-10-07
经典数学难题「方块装箱问题」（在最小正方形内互不重叠地装下 11 个单位方块）的 n=11 情形最优性证明，已用约 40 万行 Lean 代码完成形式化验证。该工作有 AI 工具（Astra、Claude）参与协助，由社区多人协作完成。同一事件的更详细版本见前一条帖子。
所属事件:11 方块装箱最优性获 Lean 机器校验证明(16 条相关)→
「研究」频道最新
- AEGIS 密码算法 Jasmin 高保障实现提速,覆盖 x86 AESNI — jedisct1 · 2026-10-07
- 新论文反驳「换性别就翻答案即偏见」：改写措辞同样会翻 — yoavgo · 2026-10-07
- IR4RL：把中间渲染进度变成 RL 奖励，Image-to-Code 达新 SOTA — phillip_isola · 2026-10-07
- MMM 优化器只 exploited 不探索,PymcLabs 用 bandit 找回流失收入 — twiecki · 2026-10-07
- ADAG 论文:全自动解读归因图, circuit tracing 告别人工 — aryaman2020 · 2026-10-07
- 研究者确认:OpenAI 成果含唯一博弈定理与阿贝尔簇有理 Hodge 证明 — aran_nayebi · 2026-10-07