Hacker News· alfiopuglisi·· 7 天前AI 评分71
Google DeepMind 用 LLM 智能体解决 9 个 Erdős 开放问题
Google DeepMind solves 9 Erdős problems
AI 导读
Google DeepMind 团队在 arXiv 发布论文，对用 LLM 生成 Lean 形式化证明来求解开放问题做了首次大规模评测。其最强智能体自主解决了 353 个 Erdős 开放问题中的 9 个，单题成本为几百美元，并证明了 492 个 OEIS 猜想中的 44 个，正被用于组合数学、优化、图论、代数几何和量子光学研究。
正文 · AI 翻译
作者：George Tsoukalas、Anton Kovsharov、Sergey Shirobokov、Anja Surina、Moritz Firsching、Gergely Bérczi、Francisco J. R. Ruiz、Arun Suggala、Adam Zsolt Wagner、Eric Wieser、Lei Yu、Aja Huang、Miklós Z. Horváth、Andrew Ferraiuolo、Henryk Michalewski、Edward Lockhart、Codrut Grosu、Thomas Hubert、Matej Balog、Pushmeet Kohli、Swarat Chaudhuri
摘要：大语言模型（LLM）在数学推理方面日益出色，但其不可靠性限制了它们在数学研究中的实用性。一种缓解方法是使用 LLM 生成 Lean 等语言的形式化证明。我们首次对该方法解决开放问题的能力进行了大规模评估。我们能力最强的智能体自主解决了 353 个开放 Erdős 问题中的 9 个，每个问题的成本为几百美元，证明了 44/492 个 OEIS 猜想，并正在被部署于组合数学、优化、图论、代数几何和量子光学研究中。一个基础智能体将基于 LLM 的生成与基于 Lean 的验证交替进行，复现了 Erdős 问题的成功，但在最难的问题上被证明成本更高。这些发现展示了 AI 辅助形式化证明搜索的力量，并揭示了实现这一点的智能体设计。
| 主题： | 人工智能（cs.AI） |
| 引用为： | arXiv:2605.22763 [cs.AI] |
| （或 arXiv:2605.22763v2 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2605.22763 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Swarat Chaudhuri [查看电子邮件]
[v1]
2026年5月21日星期四 17:24:57 UTC（1,291 KB）
[v2]
2026年6月8日星期一 12:23:48 UTC（1,301 KB）
来源：Hacker News · arxiv.org