AI 合作数学家：利用智能体 AI 加速数学家的工作

Daniel Zheng、Ingrid von Glehn、Yori Zwols、Iuliya Beloshapka、Lars Buesing、Daniel M. Roy、Martin Wattenberg、Bogdan Georgiev、Tatiana Schmidt、Andrew Cowie、Fernanda Viegas、Dimitri Kanevsky、Vineet Kahlon、Hartmut Maennel、Sophia Alj、George Holland、Alex Davies、Pushmeet Kohli
 Google DeepMind， Google

我们推出了 AI 合作数学家（AI co-mathematician），这是一个供数学家以交互方式利用 AI 智能体进行开放式研究的工作台。AI 合作数学家经过优化，能够为数学工作流程中探索性和迭代性的现实提供全面支持，包括构思、文献检索、计算探索、定理证明和理论构建。通过提供一个异步、有状态的工作空间来管理不确定性、精炼用户意图、跟踪失败的假设并输出原生数学产物，该系统模仿了人类的协作工作流程。在初步测试中，AI 合作数学家帮助研究人员解决了开放问题，确定了新的研究方向，并发现了被忽视的文献参考。除了展示一种高度交互式的 AI 辅助数学发现范式外，AI 合作数学家还在具有挑战性的问题解决基准测试中取得了最先进的结果，包括在 FrontierMath Tier 4 上获得 48% 的分数，这是所有被评估 AI 系统中的新高分。

1. 引言

数学研究是一个多维度、复杂且高度迭代的过程。虽然最终发表的成果几乎完全建立在严谨打磨的证明之上，但长期以来人们已经认识到，数学家日常工作涉及许多传统上不向公众展示的活动 [1-3]。在最终的形式化表述之下，是一个深度探索的过程：初始直觉被检验，反例被发现，核心定义和证明都经历着持续的否定与修订循环。

近年来，AI 在数学领域的能力呈现爆炸式增长，在多个不同维度上迅速扩展了该领域。在自主数学推理领域，建立在 Minerva [4] 及大量后续工作 [5-16] 的基础上，该领域现已取得突破性进展，例如自主研究系统 Aletheia [17]。在探索性搜索领域，AlphaEvolve [18, 19] 及其启发后续系统 [20-22] 允许研究人员通过持续、可引导的进化过程发现新的算法和结构。在形式化数学领域，AlphaProof [23]、相关系统 [24-36] 以及诸如 Aristotle [37] 的交互式环境已将强化学习和语言模型深度集成到经过验证的数学和开源证明助理中。与此同时，目前为商业聊天界面提供支持的推理扩展模型已经将强大的问题解决能力直接交到数学家手中。

然而，与这些系统的亲身实践经历揭示，数学研究的一个关键维度仍未得到充分支持：即将这些能力编排整合到长期、有状态、协作的工作流程中。日常的数学研究很少是一系列孤立的查询或计算机辅助证明；它涉及管理不确定性、综合来自不同领域的文献、起草和修订中间产物，并在数天或数周内跟踪复杂的、分支式的假设。

由于标准聊天界面本质上是瞬态的，而专用引擎缺乏更广泛的上下文，研究人员必须充当对话式头脑风暴、形式化证明器和计算脚本之间的手动连接组织。尽管软件开发者越来越依赖 AI 驱动的编码环境来提供这种编排能力，但这些工具基本上是针对代码的生命周期而非数学独有的抽象、证明和产物进行优化的。为了真正加速发现，我们认为 AI 辅助数学的下一阶段必须专注于这缺失的编排维度，从本质上支持数学活动中全面而“混乱”的现实。

为了理解如何为这些活动构建原生环境，我们可以更深入地研究软件工程领域。最近的进展（例如，Google Antigravity [38]、Claude Code [39] 和 OpenAI Codex [40]）已经证明了人类与智能体 AI 系统之间高效交互式协作的变革潜力。这些系统成功的原因之一是，已有的软件工程实践体现了捕捉和加速迭代探索所必需的范式。非正式软件规范（如设计文档）允许智能体在长时间内自主工作，同时保持在预定义的路径上；持续测试管道为验证提供了自动化流程；而版本控制则以专业人士熟悉的方式无缝跟踪和维护项目的不断演变状态。相比之下，数学家日常工作流程中几乎没有任何类似的活动被自动化。

为了建立这种缺失的数学智能体工作流，我们推出了 AI 合作数学家，这是一个基于最新 Gemini 语言模型的、供数学家以交互方式利用 AI 智能体进行开放式研究的工作台。

AI 合作数学家提供了一个有状态的交互式工作空间，其中项目协调员（project coordinator）智能体将复杂任务委派给并行的任务流，允许用户指导和交互于不断演变的研究过程，而不是等待端到端的自主执行完成。与其他智能体系统一样，AI 合作数学家是一个设计用于标准商用语言模型的框架，不依赖于任何自定义模型行为或训练。

重要的是，AI 合作数学家的设计旨在补充而非取代现有的前沿方法。通过建立这种有状态的架构，我们为强大的底层引擎——无论是像 AlphaProof 和 Aletheia 这样的自主推理器，还是像 AlphaEvolve 这样的进化迭代器——动态部署在人类研究者的交互循环中铺平了道路。虽然 AI 合作数学家目前仅进行有限量的初步发布，但我们的目标是开发未来产品，让更广泛的用户群体能够使用这种交互范式。

在本文的其余部分，我们将详细介绍 AI 合作数学家背后的理念和架构，并分享初步成果。第 2 节概述了我们设计交互式 AI 辅助数学的核心原则。第 3 节通过具体的实例演练，将这些原则付诸实践，重点介绍了程序化约束和对抗性评审循环如何防止系统在处理棘手问题时走捷径，以及并行任务流如何支持多方面的研究。第 4 节讨论评估诸如 AI 合作数学家等交互式数学智能体的策略。第 5 节展示了早期的定性结果，展示了实践中的数学家如何使用该系统引导开放式研究并产生可验证的见解。第 6 节评估了该系统在静态问题解决基准上的表现，为其底层能力提供了基线测量。第 7 节描述了我们在开发 AI 合作数学家过程中遇到的挑战和局限性。最后，我们概述了对下一代 AI 辅助数学的愿景。

2. AI 辅助数学的设计原则

我们设计的首要目标是支持人类数学家完成他们自己的工作。正如 Thurston [41] 著名论述所言，数学从根本上说是一项旨在推进人类理解的社会性事业，而不仅仅是生成形式化证明的机器。为了真正地加速数学家的研究，AI 工具必须融入这个以人为中心的现实。为此，AI 合作数学家的构建旨在捕捉专业数学工作流中的持久特性，同时务实应对当前 AI 推理的优势和劣势。我们的设计基于对数学实践的历史记录，以及我们在观察和改进以往数学发现系统（尤其是谷歌开发的系统）方面的经验。我们依赖七个核心原则来指导这一设计：

拥抱证明之外的数学：真正的数学发现涉及超越定理证明的复杂活动组合，例如迭代精炼研究问题、梳理文献、头脑风暴、进行大量计算和数值模拟以建立直觉等等。Putnam [42] 认为，将数学简化为孤立的形式逻辑体系忽略了该学科深刻的准经验现实，我们的设计有意识地反映并支持这种整体性的、多模态的现实，而不仅仅是最终指标——定理证明。

支持意图的迭代精炼：在许多领域，用户一开始就确切地知道自己想要什么。然而，在数学领域，发现过程高度依赖于持续的迭代和精炼。正如 Pólya [1] 在其关于合情推理的研究中所展示的那样，提出正确的问题往往需要大量的启发式猜测才能起步。正如 Georg Cantor 所言：“在数学中，提出问题的艺术被认为比解决问题更有价值”[43, p. 27]。使用 AlphaEvolve 等系统的经验也证实了这一点：数学家花费大量精力积极迭代究竟要关注哪个问题——在扩大规模之前，先用较小的运行或相关问题进行测试 [18, 19]。我们设计了一个灵活的支持多重探索路径的界面，以便用户可以流畅地精炼定义、问题和猜想。

产出原生的数学产物：研究数学家已经有标准的工作方式。AI 合作数学家不是输出短暂的聊天记录或过早润色的手稿，而是将其过程围绕一份“活的”工作论文展开。在传统工作流程中，起草和批注有助于数学家建立对项目的严谨心智模型——确切地知道哪些部分是可靠的，哪些需要进一步关注。由于自主推理系统可以在后台异步地执行大部分探索性工作，用户可能会失去这种有机的上下文。为了帮助用户重建他们的心智模型，我们的系统跟踪研究不断演变的状态，并通过内嵌文本和页边注进行可视化。通过显式地提供上下文——例如特定主张的来源或起草的引理存在的争议——系统以一种完全符合数学社区习惯的格式展示了 AI 的底层过程。

启用异步交互与灵活引导：数学研究很少是线性过程。为了模仿这一点，该系统的运作模式不是单一对话聊天机器人，而是一个异步团队。在底层，一个消息传递系统允许多个专用智能体并行工作。由于这些智能体异步运行，系统可以为一个问题分配大量计算资源而不会阻塞用户，从而让重度计算和持续交互性可以共存。

用户不会被锁定在系统“思考”的过程之外，而是可以在任何时候直接与中央项目协调员智能体沟通，以进行干预、绕过当前限制并引导正在进行的研究。这种协作是双向的：如果智能体停滞不前，项目协调员智能体会透明地标记障碍并请求人工协助以帮助系统解锁。

通过渐进式披露管理认知负荷：当用户和 AI 智能体协作探索多个并行途径、从死胡同回溯并重用中间结果时，复杂的研究会变得难以处理。如果高层次策略（例如，“尝试不动点方法”）与多个后台智能体的低层执行日志（例如，“我们必须在第 40 行验证可测性”）混在一起，一个长而无结构的聊天记录会迅速变得无法使用。为了控制向数学家揭示的信息量，我们的协作界面采用了渐进式披露，通过模仿智能体层级本身，将高层次意图与低层执行分离开来。默认情况下，用户主要与项目协调员智能体交互，后者会筛选掉专用智能体沙箱中的低层执行信息。然而，系统始终为用户提供按需深入查看任何并行智能体活动的细粒度细节的能力。

跟踪、管理和沟通不确定性：数学发现要求高标准严谨性，一个有缺陷的引理或被幻觉出的参考文献就足以破坏整篇论文。由于基础模型的推理能力容易出现不可预测的缺陷，它们的零样本输出在一个要求精确的领域引入了不确定性的基线。系统架构不是隐藏这种摩擦，而是围绕这种不确定性的生命周期进行设计。它通过维护详细的版本历史来跟踪不确定性，该历史主要由智能体使用（也可供用户使用），以监控主张如何演变或被质疑；它通过用计算换取验证（例如，通过持续评审、数值模拟和系统性引用检查）来管理不确定性；并且它通过识别评审过程在论证的特定部分何时停滞来沟通摩擦。通过使用内嵌高亮和页边注将用户注意力吸引到这些停滞的部分，系统突出了工作论文中需要更仔细人工审查的领域。通过将不确定性视为一个需要被编排的核心变量，而不是一个简单的错误状态，可以从天生不可预测的模型中合成为稳健的数学输出。

保留失败探索的历史：在数学研究中，知道什么行不通往往和知道什么行得通同样重要。虽然智能体被配置为绕过障碍，但系统接受特定目标或并行任务流可能以失败告终。架构不是静默重启或清除这些不成功尝试的历史，而是将死胡同视为一等、永久的结果。保留项目历史的这个“负面空间”对于解决困难的数学问题至关重要。通过维护失败目标和已尝试策略的持久记录，系统为用户和 AI 提供了上下文，以便基于这些失败协作地规划新的、信息更充分的任务流，这反映了反驳是数学进步基础的观点 [2]。

3. AI 合作数学家的实践：实例演练

为了展示我们的设计原则如何在实践中体现，我们将模拟一个使用合作数学家原型的代表性会话。

在此场景中，一位数学家探索计算几何中的一个开放问题：证明一个“沙发”能够同时绕过左转和右转直角弯道的面积上限。这是 Moser [44] 首次提出的一个问题的变体，其下界在最近一项关于将 AlphaEvolve 应用于数学优化问题的工作中得到了探索 [45]。

图 1 | 一个典型 AI 合作数学家工作区中智能体组织的简化图。 箭头表示用于收集信息和向用户分发指令的标准通信路径。

该系统的运作方式不是标准的对话聊天机器人，而是提供一个关联的“工作区”，存储项目的所有信息。这个工作区由智能体层级结构操作，它们将工作写入共享文件系统并通过内部消息系统进行通信。用户提供输入并与顶层的项目协调员智能体讨论想法，后者将工作委派给链条下游的其他智能体，依此类推。与人类组织非常相似，我们观察到为智能体建立沟通渠道和清晰的升级路径对于团队运作非常重要，以便它们在遇到问题时使用。图 1 展示了智能体组织的大致示意图。

3.1. 初始探索

标准的零样本 LLM 要求用户预先提供一个完美的提示词。为了体现我们支持迭代精炼意图的原则，AI 合作数学家从一个交互式的引导阶段开始，旨在帮助用户正式确定他们的意图。

在这个例子中，用户通过上传最近的一篇论文 [45] 和一些上下文到聊天界面来启动会话：“我想建立一个项目，看看我们能否为这篇论文中讨论的移动沙发问题的变体证明一些上界。”

顶层的项目协调员智能体不会立即开始寻找解决方案。相反，它会开启对话并充当“回音板”，在聊天中回复：“根据文本，Baek 已经证明了 Gerver 的下界对于经典沙发问题是紧的。然而，另外两个变体的上界仍然是开放的……您想特别关注其中一个，还是两个都关注？您的目标是证明某个特定的下界是紧的，还是仅仅建立任何新的、严格的上界？”

一旦用户澄清，项目协调员智能体就会将其对项目核心问题和高层目标的理解形式化，并呈现给用户。在详细阅读这些提议后，用户要求修改目标的措辞，项目协调员随即更新。此时，用户正式批准目标，允许项目协调员进入项目的下一阶段（图 2）。通过将初始交互视为对话，系统确保下游资源被导向数学家实际、精炼后的意图。

图 2 | 在初始探索阶段，用户与项目协调员之间的对话产生了经批准的研究问题和项目目标。

3.2. 分支研究

目标确定后，系统通过渐进式披露来管理用户的认知负荷：项目协调员智能体将工作委派给并行的任务流（workstreams），每个任务流与一个预先批准的目标相关联，并由其自己的任务流协调员智能体管理（图 3）。任务流协调员接收经批准的研究问题陈述和选定的目标，以及项目协调员选择提供的任何具体指令作为输入。每个协调员执行一系列线性动作，其中可能包括委派给专门的子智能体（图 4）。这些任务流的多样性突显了系统拥抱证明之外数学的能力。目前，我们的专门子智能体基于标准的 LLM 调用（包括 Gemini Deep Think），并未使用 AlphaEvolve、AlphaProof 或 Aletheia 等高级研究系统，但我们指出了在过程中它们自然能增加价值的点。

这里我们描述的場景是项目协调员智能体为每个目标启动一个任务流，但也可以为每个目标定义多个任务流，或者在某些目标依赖的工作完成之前，暂不为它们启动任务流。

目标 1：文献综述：一个任务流协调员智能体委派给一个专门的文献综述子智能体。利用我们计算密集型搜索工具，它发现了包含沙发问题上界先前所用方法的关键论文。根据重要参考文献的指引，它使用特定的网络和文献访问工具直接查询这些论文，以识别关键结果的确切陈述和证明。

目标 2：计算框架：另一个任务流协调员智能体负责设计所需计算框架的任务。根据先前文献中观察到的策略，该任务流协调员智能体首先设计计算框架的高层逻辑，使用子智能体创建工具派遣 Gemini Deep Think 来证明这可以按要求给出严格的上界。一旦证明完成，它使用另一个子智能体创建工具创建一个编码智能体，指示其实现所需的 Python 库以及相关的测试和演示案例。当这些智能体各自提供状态更新时，任务流协调员智能体会异步更新用户端的任务流报告，添加证明的细节并提供关键代码文件的链接。

图 3 | 一旦研究问题和目标被定义，项目协调员就会安排任务流以实现目标。 每个目标可能附加多个任务流，并且可以在研究过程中的任何时候添加新的任务流，例如响应用户的特定请求。每个任务流旨在生成一份经过充分评审的报告，附带附件和外部参考文献，并提供增量的进度报告，用户可以在工作进行时阅读以判断部分进展。任务流可能因多种原因未能完成其工作，在这种情况下，会向用户显示一个醒目的警告以及增量报告。

现有系统中的所有证明都是非形式化的，但添加诸如 AlphaProof 的形式化证明器的可能性，将能提高那些能用现有形式化数学库陈述和证明的命题的正确性可信度。或者，使用更强的非形式化证明系统（如 Aletheia）将显著增强系统的能力，但会带来相应的计算成本。

目标 3：执行搜索：最终的分支定界搜索在另一个任务流中执行，该任务流由项目协调员智能体在计算框架任务流成功完成后创建。共享文件系统允许此任务流协调员智能体导入先前任务流中开发的库，现在它使用并行代码执行工具将搜索扩展到单个脚本之外。并行代码执行请求在单独的云机器上运行，避免了用户设置或访问本地集群的负担。搜索结果被整理到一个文件中，该文件附加到任务流报告，摘要信息和结论被写入报告的正文。

在当前原型中，此类计算搜索是通过标准智能体原语的组合来执行的，但添加诸如 AlphaEvolve 的进化搜索算法将为这种优化和搜索例程提供一个“超强引擎”。

图 4 | 一个任务流由任务流协调员智能体采取的一系列动作组成，这可能导致项目状态和/或用户界面的更新。 在这个简化的示例轨迹中，任务流协调员先进行文献搜索，然后进行特定的网络查询，每次之后都用发现更新报告。随后，收到来自项目协调员的消息，传达了用户的请求，这导致报告进一步更新。然后，任务流协调员将最新报告送交评审。如果评审成功通过，协调员就可以将其工作标记为“完成”。

3.3. 交互式引导与硬约束

当负责解决困难的研究问题时，标准 AI 智能体常常会找到无效的捷径、幻觉出引理、对细节含糊其辞并过早声称成功。AI 合作数学家的一个决定性技术特点就是应用程序化硬约束来防止这些失败模式，并结合用户的主动人工引导。

在计算探索过程中，如果搜索空间爆炸，最初提出的朴素回溯方法可能会失败。在这种情况下，编码子智能体受到严格规则的约束：它不能将代码标记为完成，直到其测试通过并且评审智能体接受代码和测试中“黄金值”的有效性。由于评审智能体反复拒绝失败的代码，任务流协调员智能体被阻塞。系统不会静默重启，而是将这次失败的探索作为持久记录保存在共享文件系统中，供项目协调员读取。

由于被迫管理和披露其不确定性，项目协调员智能体向用户发出警报，并在聊天中明确请求帮助：“我们最初的搜索实现效率不足以找到我们需要的结果，而且文献中也没有太多其他例子。您是否有更好的数学直觉，可以提供一种我们可以应用的剪枝策略？有关当前方法的更多详细信息可以在以下文档中找到。”

至关重要的是，用户不会在智能体工作时被锁定。通过聊天界面，用户阅读项目协调员的更新并主动引导项目，发送消息建议一个拓扑剪枝启发式方法，并指示协调员在当前工作正在进行时创建新的任务流来研究新的界限策略。

3.4. 最终输出

在用户引导系统度过计算瓶颈之后，各个任务流完成了它们的具体目标。然而，最终的输出不是短暂的聊天消息。每个任务流协调员智能体负责生成一份编译好并经评审的 LaTeX 文档作为其主要输出，当用户打开该任务流时会 prominently 显示该文档。

为了产出自然的数学产物，我们要求协调员在这些文档中满足特定标准：

• • 阐述：草稿必须包含对导致该结果的研究过程的解释，而不仅仅是最终结果。
• • 页边注释：文档利用页边注提供附加信息，明确地将主张链接回工作区。注释可能写道：[剪枝启发式方法源自用户建议；基线界限 2.2195 来源于 arxiv.org/abs/... 上的论文]。
• • 内部链接：除了外部文献外，还会引用智能体创建的内部文档，为用户提供直接入口点来审计共享文件系统。
• • 评审过程：在报告能被标记为最终定稿且任务流完成之前，报告必须提交给论文评审过程，由多个 AI 评审员智能体对其内容和风格进行审查，所有这些评审员都拥有交叉检查参考文献、代码输出以及逻辑正确性的工具和能力。评审员智能体在评审轮次之间持续存在，形成一个迭代过程，报告在此过程中得到精炼和改进，只有当所有评审员正式批准报告时，该过程才告结束。为了避免无限循环，如果任务流协调员智能体无法通过评审过程，它可以将此问题上报给项目协调员智能体。在这种情况下，任务流被标记为未完成，并将上报消息清晰呈现给用户，使用户能够立即理解该报告可能包含未解决的问题。

4. 交互式数学智能体的评估

从历史上看，AI 辅助数学的进展是通过静态问题解决基准来衡量的。如今，该领域严重依赖此类基准，包括 IMO ProofBench [46]、FrontierMath [47] 和 PutnamBench [48]，而其前身 MATH [49] 和 GSM8K [50] 在衡量早期 LLM 进展方面极具影响力。

然而，随着前沿系统在原始问题解决能力上已达到或超过人类专家水平 [例如，51, 52]，我们认为继续提高这种能力的增量价值正在减少，并且 AI 辅助数学的进展现在至少部分受限于反映专业数学家更广泛工作流程的其他能力。

这意味着，首先，AI 系统应该根据更广泛的任务来衡量。诸如用于通用事实查找的 DeepSearchQA [53] 和用于在竞赛数学证明中查找错误的 Hard2Verify [54] 等基准，衡量了与数学研究过程中精确类似的能力。但据我们所知，尚未有为专业研究数学环境开发类似的基准。随着 AI 系统的改进，对这些辅助能力的清晰衡量（以及针对它们的改进！）将变得越来越重要，以降低“锯齿状前沿”[55] 的严重性以及与之相关的人类驱动与 AI 驱动数学之间的阻抗不匹配。

然而更重要的是，我们认为，AI 辅助数学系统在默认情况下应被视为人机协同系统，其进步和成就应相应衡量。这呼应了我们的设计原则，即我们系统的首要目标是协助数学家完成其工作，而不是独立于他们取得成功。基于此框架，我们首先展示了数学家直接使用 AI 合作数学家产生的结果（第 5 节），然后测量了 AI 合作数学家的静态问题解决性能（第 6 节）。

5. 与数学家的早期成果

作为我们让交互式工具更广泛可用的一部分，我们已经向少数专业数学家提供了 AI 合作数学家，供他们用于自己的研究。早期用户探索的广泛用例反映了该系统的广泛适用性以及融入标准研究工作流程的能力。AI 合作数学家已在多种情况下充当了功能性辅助工具，例如导航不相关的文献、进行数值实验以及在数学多个领域获得证明。在本节的剩余部分，我们将展示几个用例，说明该系统在当前有限发布中由近期用户获得的实用性。需要说明的是，虽然许多用户与 AI 合作数学家的成功互动带来了新颖的发现，但对该工具的反馈和满意度各不相同，其他用户发现它对自己的工作不那么有效。我们将在第 7 节讨论其中一些挑战，并希望利用这些数学家的经验和反馈来指导未来的基准测试和开发方向。

值得注意的是，这里展示的所有成果都是由数学家直接使用该工具独立产生的，没有 GDM 研究人员的任何监督或干预。

5.1. 案例研究：一个 Kourovka 问题

早期用户 M. Lackenby 使用 AI 合作数学家研究了拓扑学和群论中的几个问题。他的工作解决了一个开放问题（Kourovka 笔记本中的问题 21.10）。Lackenby 在此案例中的过程说明了“数学家参与其中”交互方式的价值。

Lackenby 开始时只是简单输入了问题陈述；系统确认了含义，然后创建了两个独立的任务流，一个试图证明该结果，另一个试图反驳它。首先返回的结果是一个被系统自身标记为不正确的“证明”——一个任务流写出了一个论证，但随后一个评审员智能体发现了一个缺陷。然而，在查看这篇论文时，Lackenby 意识到尽管存在这个缺陷，但它包含了他所说的“一个非常非常聪明的证明策略”。此外，当他阅读评审员对证明的批评时，他意识到：“等一下，我知道如何填补这个空白。”

他指出了修正论证的方法，系统得以写出完整且正确的证明。最后，Lackenby 下载了文档并应用了自己的修订——推广了结果并添加了例子——然后再次上传并要求项目协调员创建一个任务流进行最终评审。系统照做了，发现了论文中的两个小问题，他在最终版本中进行了修复。

从这个案例中得到的一个教训是，AI 和数学家之间的来回交互对于解决问题至关重要。对 Lackenby 来说，这表明“当用户熟悉该领域时，该系统效果最佳。”虽然这也许被看作是一种限制，但他补充道：“让它解决一个我完全不了解的问题有什么意义呢？”

智能体动作：
在幕后，该任务流的协调员智能体：

• • 创建了一个编码子智能体来执行对“非 just-finite 表示”的计算搜索，并成功找到了两个例子。
• • 分析了这些例子并执行文献搜索，以识别与其构造相关的理论，从而产生了一个生成非 just-finite 表示的通用方法。
• • 注意到这并没有否定该猜想（因为群可能有多个表示，找到一个非 just-finite 表示并不意味着没有一个表示是 just-finite 的），但决定在此结束其任务流，基于该论证提出了一个更精确的猜想，并将报告送交评审。
• • 作为评审过程的一部分，与评审员智能体开启了来回讨论。在此过程中，一个评审员智能体发现了一个可以用来正面证明该猜想的方法。
• • 同意了评审员的意见，并将任务流转向撰写这个方法。经过进一步评审，产生了 Lackenby 进行补充以完成证明的草稿。

5.2. 案例研究：Stirling 系数

另一位早期用户 G. Bérczi 使用 AI 合作数学家时，最初是解决一个关于对称幂表示的 Stirling 系数行为的问题。具体来说，猜想假设在某个二项式展开中，系数不仅是严格正的，而且形成一个对数凹序列。

为了启动项目，Bérczi 准备了一份简短的说明，介绍了该主题、猜想的背景以及已知方法。这份入门材料还包括了他之前使用其他系统（如 AlphaEvolve）进行实验后得出的建议方向。虽然 AlphaEvolve 未能解决更高阶的情况，但它暗示了恢复系数归纳公式的可能方向。Bérczi 将此包含在他的文档中，作为初始项目制定讨论的一部分。Bérczi 称之为“结构化提问”的这种提供深度、丰富背景的风格，是他发现对其他 AI 系统也有效的方法。

针对 Bérczi 的问题，AI 合作数学家分别在两个任务流中为其中两个猜想建立了证明（目前正在详细的人工审查中）。它还为其主张以及对未证明猜想的调查提供了详细的计算证据。Bérczi 指出，系统的设计在多个方面提供了帮助。不仅很容易跟踪那些勾选任务的“绿色对勾”，更重要的是，最终文档中的一条边注评论提醒了他一个关键的见解，他可以在聊天界面中就此提问。尽管如此，他指出与 AI 系统协作需要一些技巧，他说“现在使用这个并不简单”，并建议“数学家之间如何使用这些模型将会产生巨大的差异。”

智能体动作：
两个关键任务流提供了所述猜想的证明。为了说明工作流，在第一个任务流中，协调员智能体：

• • 创建了一个编码子智能体来执行对展开式的初始计算枚举，其规模控制在几分钟内合理运行。
• • 从结果中观察到，该猜想在原陈述下对  是假的，但对更大的  似乎成立，并且其最初的证明策略是无效的。
• • 使用 Gemini Deep Think 子智能体为更新后的猜想提出新的证明策略。它成功做到了，说服了任务流协调员智能体，随后也说服了评审员智能体。

5.3. 案例研究：哈密顿系统中的一个引理

AI 合作数学家的第三位早期用户 S. Rezhchikov 提出了他在研究中遇到的一个近期技术性子问题，主题是关于一类特定哈密顿微分同胚的具有某些便利性质的扰动是否存在。

使用该系统，Rezhchikov 与项目协调员智能体讨论了这个问题，并提供了包含与问题陈述相关结果的补充论文，直到任务的确切定义达成一致，并创建一个任务流来尝试解决它。该任务流生成的文档包含一个关键引理，其证明简洁优雅，经受了仔细检查，并基本解决了 Rezhchikov 提出的问题。Rezhchikov 再次指出，其他 AI 系统在相同提示下未能证明该结果，尽管在没有多次采样尝试和受控条件的情况下，很难从这种个别实验中得出结论。

Rezhchikov 还提出了另外两点观察，阐明了该系统的价值。一点是关于探索一种似乎不起作用的方法：这里的附加价值在于，系统让他比其他人更快地到达了死胡同。正如他所说：“我本可以轻松地花一周时间在那里幻想可能存在什么，但相反，我直接继续前进了。”另外，他注意到正确证明的质量似乎相对较高：“从美学上讲，我会将其证明的普遍风格评价为我使用过的所有模型中最好的。”

这说明了 AI 合作数学家如何帮助数学研究人员以一种自然融入他们典型探索性研究工作流的方式探索想法。

智能体动作：
在此案例中，任务流协调员智能体：

• • 使用专门工具进行了文献综述，了解所讨论问题的常用技术和陷阱，这突出了除 Rezhchikov 提供的之外需要注意的几个关键性质。
• • 进行了具体的后续文献查询，以理解这些要点的确切性质。
• • 将问题陈述和关键上下文信息传递给 Gemini Deep Think，后者生成了包含关键引理的证明，随后被写入报告。

6. 问题解决基准测试结果

尽管我们主张进行更广泛的能力衡量，但我们也承认问题解决基准目前是衡量 AI 系统在数学领域性能的最佳客观指标。在本节中，我们将讨论使用此类基准来衡量 AI 合作数学家性能的尝试。

由于 AI 合作数学家设计为通过长篇报告传达结果并在卡住时向用户提问，我们开发了一种自定义模式，系统在该模式下无法接收初始问题之外的任何外部输入，并在用户聊天面板中返回单个最终答案。为此模式实现的主要区别包括：

• • 绕过初始的问题定义对话，假设所有必要信息都已包含在问题陈述中。
• • 硬编码一个单一的项目目标：“解决问题”。
• • 引入固定时间限制，之后如果项目协调员智能体尚未给出答案，则必须给出最终答案。内部评估设置为 24 小时，FrontierMath 设置为 48 小时。大多数问题尝试在此时间限制内完成，但对于没有人工干预的难题，系统有时会在此之后继续运行，尤其是在难以生成清晰解决方案的情况下。

作为一个长期运行的智能体系统，与通常在这些任务上评估的基础模型相比，AI 合作数学家使用了相应更多的计算量。然而，尽管 AI 合作数学家解决方案尝试中没有明确的推理限制，但该系统的开发效率足以服务许多外部用户。我们观察到，每次尝试使用的模型和工具调用次数，大致与一个长时间的 AI 辅助软件工程会话相当，与其作为交互式智能体工具的主要用例匹配。

6.1. 内部研究数学评估

我们在一个内部基准上测试了 AI 合作数学家，该基准包含 100 个未泄露的研究级数学问题，其答案可通过代码检查，这些题目来自专业数学家。

在这些基准上，AI 合作数学家的性能显著优于单次调用 Gemini 3.1 Pro 模型和单次调用 Gemini Deep Think 系统（图 5）。如前所述，AI 合作数学家也使用了更多的计算量：实际上，AI 合作数学家底层的许多内部智能体都构建在 Gemini 3.1 Pro 之上，而证明智能体可以利用 Gemini Deep Think。

分析具体例子，我们看到了 AI 合作数学家各个特性的优势。

在一个关于几何平铺的问题中，我们看到 AI 合作数学家成功地将问题的核心简化为一个布尔可满足性问题，并使用 PySAT 库解决。为了这种框架能工作，需要对核心问题进行几项非平凡的调整——这种解决方案显然有利于拥有持久文件系统和智能体代码编写能力的系统。尽管其他模型的评估框架允许执行代码，但它们很难开发和测试更复杂的库。Gemini 3.1 Pro 和 Gemini Deep Think 都尝试用纯理论方法解决这个问题，但在此例中这显然是一个更困难的任务。

在一个关于表示论的问题中，AI 合作数学家利用其文献搜索工具，正确地从相关论文中检索出确切的定理陈述，并将其应用于解决问题。其他模型则尝试应用更一般的定理；尽管这些定理与主题领域相关，但由于无法访问文献来检查精确的陈述，它们无法将定理条件与问题中存在的假设正确匹配。

在一个同时涉及理论和计算方面的组合学问题中，我们看到 AI 合作数学家将其工作清晰地分为多个任务流，将解决方案的理论基础与代码开发分开精炼。在理论任务流中，评审员在运行抽查时指出了多个逻辑错误和不一致之处（与其他模型犯的错误类似），这些错误最终在最终的任务流报告中得到纠正，使得项目协调员能够干净利落地组合各个部分，给出正确的解决方案。

图 5 | Gemini 3.1 Pro、Gemini 3.1 Deep Think 以及 AI 合作数学家（同样基于 Gemini 3.1）在一个内部研究数学基准上的准确率得分。

6.2. FrontierMath

一个自然的比较是外部的 FrontierMath 基准 [47]。Epoch AI 在上述最终答案模式下对 AI 合作数学家在该基准的 Tier 4 上进行了测试。用 Epoch AI 的话说：“这个极高端由 50 个问题组成，由教授和博士后设计为短期研究项目。其难度旨在超越 Tier 3，其中一些问题可能在未来几十年内都未被 AI 解决。”来自所有主要提供商的前沿模型和系统都会定期在 FrontierMath 基准上进行测试。

评估是盲测进行的，Epoch AI 可以直接访问 AI 合作数学家的用户界面，他们自己输入问题并检索答案，系统开发人员在评估期间既看不到问题也看不到项目工作区的状态。

在排除两个公开的示例问题后，AI 合作数学家在该基准上取得了新的高分，正确解决了 48 个问题中的 23 个，准确率为 48%。值得注意的是，这比其所基于的 Gemini 3.1 Pro 基础模型（实现了 19% 的准确率）有显著提高，这表明我们并行的研究分支、强制评审循环和工具实现带来了问题解决任务效果的提升。正确解决的问题包括三个此前未被任何评估系统解决的问题，不过 AI 合作数学家也未能解决两个此前已被至少一个系统解决的问题。

与先前评估的一个重要区别在于，FrontierMath 评估通常使用 Epoch AI 开发的标准智能体框架执行。该框架提供对 Python 解释器的访问，但也对智能体轨迹中使用的 token 数量设置了硬性限制（就相关模型 API 中所计入的而言）。然而，在我们的设置中，我们只使用自己的工具实现，并且对模型调用或生成的 token 数量没有限制。这意味着我们的系统可能比先前评估的系统具有更高的推理成本。

7. 挑战与局限性

虽然 AI 合作数学家展示了交互式 AI 工作流的潜力，但我们在使该系统真正有用方面遇到了若干困难。

取悦评审员的偏差（虚假共识）：迭代评审过程是一个动态系统，它会不断演变工作文档。当一个智能体生成了一个它无法真正修复的有缺陷的论证时，满足评审员智能体的严格约束有时会导致这个系统收敛到一个仍然有缺陷的论证上，但评审员智能体再也无法检测到错误。这类论证对人类来说也可能难以拆穿，这已被强调为当前 AI 系统的一个局限性 [57]。文献中已经注意到了证明器-验证器动态中的类似病态表现 [58]。虽然这种行为相对罕见，但它违反了我们在核心原则中明确承认不确定性的要求。

棘手的分歧（非终止）：相反，当迭代评审过程无法达成共识时，它可能完全无法终止。在这种动态下，迭代评审过程会陷入无休止的修订和拒稿循环。在连续多次自主迭代中，这个循环通常会退化为越来越严重的幻觉推理——一种俗称“死亡螺旋”的现象。虽然我们实现了各种机制来减轻这些影响，但语言模型之间频繁相互分歧的核心问题依然存在。早期用户已经注意到这种行为，学会了识别任务流何时进入这种状态，并相应降低对其输出的信任度。

系统自主性要求让渡控制权：数学研究本质上是探索性的；预定义任务规划通常是不可能的，因为发现正确的步骤序列等同于解决问题本身。因此，模型总是面临遭遇计划外困难的重大风险，而在 AI 合作数学家中，我们允许系统在没有中间人工输入的情况下自主运行许多小时，这放大了这种风险。从我们的经验来看，当前模型在此类情况下的判断力远落后于人类的能力和期望，而要在允许长期自主能力的同时保持用户的可控性，这是一个具有挑战性的平衡行为。

表征的语义含义：我们的团队很早就认识到，数学家倾向于将排版精美的文档与相应水平的内容严谨性联系起来，这种直觉与 LLM 的表现相悖，LLM 擅长生成完美的 LaTeX 格式，但经常在严格的逻辑验证上遇到困难。在 AI 合作数学家中，我们试图通过将输出强调为带有相关边注的“工作文档”来减少这种误解，但似乎可以开发新的界面来更直观地表示此类文档的特征。最近在 HCI 领域的 AI 赋能研究 [例如，59] 可以为前进的道路提供灵感。

此外，将功能强大的智能体系统引入数学领域也带来了一些风险。向前发展，社区必须应对几个系统性的挑战：

维持文献中的信噪比：随着 AI 系统在 LaTeX 排版和文献综合方面变得高度熟练，社区将需要管理潜在的自动化输出涌入。如果这些工具经常被用作自治生成器而非人工引导的合作者，该领域将会出现看似合理但内容浅薄、增量式或带有细微缺陷的论文增长。这种转变可能会增加系统性的“语义噪音”，要求研究人员开发新的启发式方法，以便在更高基线量的草稿中有效识别真正新颖的数学发现。形式化方法和自动形式化可能有助于检查正确性和突出论文中的缺陷，但无法替代社区成员理解和吸收新发表作品含义的过程。

调整同行评审生态系统：数学同行评审过程依赖于深入、密集的人工验证。智能体 AI 引入了一个具有挑战性的新规模动态：一个系统可以在几分钟内生成一个 20 页的证明尝试，但一位人类专家可能需要几天时间来验证它。如果 AI 辅助起草变得无处不在，却没有内置的、可审计的论文轨迹，这可能会给志愿同行评审系统带来沉重且不成比例的负担。AI 合作数学家的页边注是为提高结果可审计性迈出的微小第一步，但需要更广泛的社区标准。此外，尽管我们的系统具有专门的评审员智能体，但用 AI 替代人类评审员也带来了自身的风险。虽然自动化评审员擅长局部逻辑检查、捕捉代数错误或找出缺失的引用，但它们目前缺乏判断一篇论文的优雅性、深度或真正数学意义所需的整体直觉。过度依赖 AI 进行同行评审可能会导致数学评估被简化为机械验证，可能边缘化引导该领域的定性人类判断。

8. 结论

AI 社区最近已经跨越了多个技术里程碑，在各种数学基准测试中展示了与人类相当或超人的表现。然而，如果我们想真正加速科学发现，解决静态的、定义明确的问题只是解决方案的一部分。数学研究的前沿不是线性的对话或一系列不相关的谜题；它是一个由未经证实的直觉、分支式假设和复杂的人类协作所定义的、混乱的、重叠的、高度迭代的过程。

AI 合作数学家的设计旨在满足研究人员的真实需求。该系统没有被简化为一个孤立的“神谕”或一个简单的验证管道，而是作为一个整体的工作空间。通过管理不确定性的生命周期、通过分层委派来镜像人类工作流程，并将其输出扎根于原生数学产物，它将强大的基础模型提升为自然的协作者。通过程序化硬约束和持续维护一份“活的”工作论文，该系统确保整个研究历程——失败的测试、综合的文献、思想的持续精炼——都被捕获、审计并明确传达给用户。正如早期用户解决开放问题和发现新证明所证明的那样，这种双向交流使人类能够有效地引导 AI 度过难关。

然而，要实现这种范式的全部潜力，需要 AI 社区衡量成功的方式发生转变。虽然这些基准在评估模型生成最终答案以解决精心设计的问题方面表现出色，但它们并未捕捉到前沿研究的全部范围。它们并非旨在衡量系统交互式地修剪假设树、综合小众文献或在扩展失败时适当地停止并披露不确定性的能力。

如果我们想要构建真正充当“合作数学家”的系统，我们必须开发互补的评估框架，用以衡量协作效能、状态化探索以及不确定性的严格管理。AI 辅助数学的下一次革命将不仅仅由哪个模型能最快地综合出正确答案来定义，而将由哪个系统能最有效地帮助人类研究人员驾驭未知来定义。