Astra 和 Claude 证明了 11 个正方形的最优装填问题（已在 Lean 中形式化）

Reddit r/singularity 论文
formal-verification lean square-packing ai-assisted-math combinometry geometry claude

摘要

Astra 和 Claude 协助证明了 11 个正方形的已知最佳装填是已知最优的，该结果已完全在 Lean 证明助手中形式化。这是 AI 辅助数学与形式化验证的又一个里程碑。

https://x.com/ManassehA06/status/2107508501610217640
查看原文

相似文章

正方形中的正方形

Hacker News Top

一个展示已知最优单位正方形装填到更大正方形中的网页，包含针对不同数量正方形的交互式SVG示意图。

@yoheinakajima：如果你好奇这是否能推广……是的，作为一种装填方法可以。总体上不是最好的，但它能找到装填方案……

X AI KOLs Timeline

Yohei Nakajima 分享了“从软到刚”（硬化）方法，这是一种用于全等形状装填的形状延拓搜索方法，通过将内切圆盘逐步变形为目标形状，在正方形中找到其他方法遗漏的装填方案，但总体而言，它并不是更好的默认选择。该研究提供了公开论文、代码仓库和可重放的实验，支持完整复现。