一句话

AI Agent独立解决了9个开放 Erdős 数学问题、证明了44个 OEIS 猜想，成本仅数百美元一个——数学研究正在迎来 AI 证明时代。

怎么做到的

论文让LLM生成形式化证明（用Lean语言），再由Lean引擎验证。每次证明尝试形成一个"生成-验证"循环，最强大的Agent在这个循环中自主解决了9个开放 Erdős 问题，涉及组合数学、图论、代数几何等多个方向。 研究人员还验证了另一个规律：让AI交替进行LLM证明生成和Lean验证，结果复现了Erdős成就，但难题上成本更高。

关键数据

  • 单个Agent自主解决9个开放Erdős问题，每个问题成本仅数百美元
  • 证明44/492个OEIS数列猜想
  • 已在组合数学、优化、图论、代数几何、量子光学等领域落地使用

观点

过去我们谈AI解题，更多是考试、竞赛。现在它开始撬动真实的开放数学问题了。这个量级不一样——开放Erdős问题是经过几十年学术筛选剩下的硬骨头，能解出9个说明AI已经能在真实科研链条上承担角色。 当然，"几百美元解一个问题"在经济账上还很贵，离真正替代数学家还很远。但趋势已经明确：AI不是来考试的工具，而是来参与研究的合作者。

参考链接

arXiv:2605.22763 | https://arxiv.org/abs/2605.22763