arXiv:2605.22763：AI智能体结合Lean验证解决9个开放Erdős问题和44个OEIS猜想

2026年5月21日发布的arXiv预印本提出了首个关于LLM在Lean定理证明器中自主生成形式数学证明的大规模评估，应用于开放Erdős问题和整数序列在线百科全书（OEIS）中的猜想。由20名研究人员组成的团队——包括DeepMind和MIT CSAIL的成员——展示了一个高级智能体自主解决了353个开放Erdős问题中的9个，并证明了492个OEIS猜想中的44个。

Lean是什么，为何它对这种方法至关重要？

Lean是一个证明辅助工具，一种将数学证明写作类型并由编译器自动验证的编程语言。与可能包含通过同行评审的微妙错误的非正式数学文本不同——Lean证明要么编译通过（那么数学上是正确的）要么不通过（那么被拒绝）。验证中没有人为错误的余地。

这一特性对AI系统至关重要。LLM可以生成看起来令人信服但包含错误的数学文本；如果没有自动验证，人类数学家必须手动检查每个证明，这是瓶颈所在。有了Lean，系统生成候选证明，Lean在毫秒内验证它们——如果不编译，系统迭代；如果编译，证明是绝对正确的。

Erdős问题集是什么，为何重要？

Erdős问题是Paul Erdős（1913-1996）在其职业生涯中提出的一系列开放数学问题。涵盖离散数学、数论、组合数学、图论和极端组合学。许多带有Erdős承诺的现金奖励（25到10,000美元）。Erdős Problems服务项目维护了约800个此类问题的列表，作者从中选择了353个可以在Lean中表述的问题。

在353个问题中，自主智能体解决了9个（2.5%）——作者将其归类为可通过结构性论证或足够小的空间穷举搜索解决的「低层次」Erdős问题。「低层次」并不意味着微不足道——这些问题已开放数十年，只是不需要智能体不具备的天才式组合直觉。这些结果与Erdős Problems管理员协调，后者对其进行了独立确认。

智能体如何结合LLM生成和Lean验证？

智能体具有循环架构。步骤1：LLM（作者指定了具有形式数学微调的DeepMind内部前沿模型变体）读取Lean中的问题表述并生成关于证明结构的假设。步骤2：智能体通过Lean编译该假设——如果编译通过，返回成功；如果不通过，Lean返回特定错误（如「未知标识符」、「类型不匹配」、「策略失败」）。步骤3：智能体将该错误反馈给LLM并指示迭代。步骤4：如果5次迭代失败，智能体将问题分解为更小的引理并尝试单独解决。

作者强调智能体并非进行漫无目的的搜索——Lean编译器的反馈以一种对人类来说需要数月的方式构建了搜索，而智能体在数小时内完成。典型解决的Erdős问题需要200-500次LLM调用，在8×H100设置上需要3-12小时的实际时间。

OEIS是什么，那部分结果如何？

OEIS（整数序列在线百科全书）是一个包含超过380,000个整数序列及其描述、公式和猜想的数据库。OEIS中的许多猜想被表述为「这个序列可能由公式F生成，但尚未证明」。作者选择了492个这样的猜想，让智能体尝试正式证明每一个。

智能体证明了44个（8.9%），作者再次与OEIS维护人员协调以纳入官方记录。大多数已证明的猜想涉及递归序列的封闭形式或源于已证明的更大结果的辅助恒等式。智能体未能解决的猜想大多需要智能体未能自主发现的组合双射或结构性论证。

这对数学研究意味着什么？

作者并不声称AI智能体取代数学家。他们声称现在有一个可操作的助手，可以处理形式化证明中的「低悬果实」——这使研究人员能够专注于需要人类创造力的问题。下一步包括开发能够基于模式识别提出新猜想的智能体，以及将智能体与Lean Mathlib库（90,000+形式化定理）集成以获得更丰富的参考框架。