Rohan Paul@rohanpaul_ai · XDeepMind 把 AI 的'数学直觉'塞进 Lean 编译器里，每步都必须编译通过，结果解决 9 个 Erdős 问题，失败也暴露了隐藏错误。这篇论文重新定义了 AI 做数学的范式。
Google DeepMind提出了AlphaProof Nexus系统，它将大型语言模型与Lean形式化验证工具相结合。该系统允许LLM在生成证明的过程中，不断读取Lean的编译错误并进行修正，还可调用更强的工具辅助解决子问题。这一机制迫使模型将每一步逻辑都转化为可编译、可验证的代码，从而将其角色从“令人信服的叙述者”转变为“候选方案生成器”。在针对353个Erdős问题和492个开放猜想的测试中，系统成功解决了9个Erdős问题并证明了44个序列猜想。该研究展示了形式化验证在暴露AI逻辑错误、建立“人类提问-模型探索-验证器把关”新分工中的关键作用。
Google DeepMind 的新论文。
研究表明，AI 现在可以搜索形式化数学证明，但仅限于精心构造的受限世界。
令人瞩目的结果并非系统“像数学家一样思考”，而是它始终强迫自己的思路通过 Lean 进行形式化验证——每一步都必须通过编译检查。
问题在于，大语言模型在数学上可能听起来很有说服力，却仍会犯细小错误，因此作者使用了 Lean——一种检查每个逻辑步骤的证明系统。
他们的系统 AlphaProof Nexus 让大语言模型持续编辑形式化证明、读取编译器错误提示、重新尝试，有时还会就较小的子问题向更强大的证明工具求助。
更强的版本还维护了一个共享的局部证明尝试池，评估哪些尝试更有前景，并利用这些尝试来指导后续搜索。
这改变了模型的作用：从有说服力的讲述者，转变为候选方案的生成器——一旦出错就能被快速淘汰。
验证器并非可有可无的附加组件，而是让探索变得可容忍的机制。
没有它，一个漂亮的证明草图可能隐藏一个错误的引理；有了它，模型必须将洞见转化为可执行的逻辑，否则就会直观地失败。
作者在真实未解决的数学问题上测试了该系统，包括 353 个形式化的 Erdős 问题和 492 个来自整数序列在线百科的开放猜想。
主要结果是，最佳智能体解决了 9 个 Erdős 问题，证明了 44 个序列猜想，同时还协助解决了优化、图论、代数几何和量子光学领域的问题。
失败与成功同样具有启示性——因为智能体有时将难点藏在一个辅助引理中，或幻觉出一个已知结果，而这正是形式化检查旨在暴露的那类错误。
真正的转变并非数学上的完全自主，而是一种新的分工：人类选择形式化问题，函数库定义领域，模型提出路径，而证明助手不为所动。
----
"借助 AI 驱动的形式化证明搜索推进数学研究"
论文链接 – arxiv.org/abs/2605.22763