AI协数学家：以智能体AI加速数学研究

Daniel Zheng

\thepa

Ingrid von Glehn

\thepa

Yori Zwols

\thepa

Iuliya Beloshapka

\thepa

Lars Buesing

\thepa

Daniel M. Roy

\thepa

Martin Wattenberg

\thepa

Bogdan Georgiev

\thepa

Tatiana Schmidt

\thepa

Andrew Cowie

\thepa

Fernanda Viegas

\thepa

Dimitri Kanevsky

\thepa

Vineet Kahlon

Google

Hartmut Maennel

\thepa

Sophia Alj

\thepa

George Holland

\thepa

Alex Davies

\thepa

Pushmeet Kohli

\thepa

摘要

我们推出了AI合作数学家，这是一个供数学家交互式利用AI智能体进行开放式研究的工作台。AI合作数学家经过优化，能够为数学工作流程中探索性和迭代性的现实需求提供全方位支持，包括构思、文献检索、计算探索、定理证明和理论构建。该系统通过提供一个异步、有状态的工作空间来管理不确定性、细化用户意图、追踪失败假设并输出原生数学产物，从而模拟人类协作工作流程。在早期测试中，AI合作数学家帮助研究人员解决了开放性问题，识别了新的研究方向，并发现了被忽视的文献引用。除了展示一种高度交互式的AI辅助数学发现范式外，AI合作数学家还在困难问题求解基准测试中取得了最先进的结果，包括在FrontierMath第四层级上获得48%的得分，这是所有已评估AI系统中的最高分。

1 引言

数学研究是一个多维、复杂且高度迭代的过程。尽管发表记录几乎完全建立在精炼、严谨的证明之上，但数学家的日常工作长期以来被认为涉及那些传统上不对外公开的活动[undef, undefa, undefb]。在最终的形式化体系之下，隐藏着一个深度探索的过程：初始直觉在此过程中被检验，反例被发现，核心定义和证明都经历着持续的反驳与修正循环。

近年来，人工智能在数学领域的能力呈现爆发式增长，迅速从多个不同维度拓展了该领域。在自主数学推理方面，基于 Minerva [undefc] 等早期系统以及其后大量研究工作 [undefd, undefe, undeff, undefg, undefh, undefi, undefj, undefk, undefl, undefm, undefn, undefo] 的积累，该领域现已取得突破性进展，例如自主研究系统 Aletheia [undefp]。在探索性搜索方面，AlphaEvolve [undefq, undefr] 及其启发下的系统 [undefs, undeft, undefu] 使研究人员能够通过持续、可引导的演化过程发现新颖的算法和结构。在形式化数学方面，AlphaProof [undefv]、相关系统 [undefw, undefx, undefy, undefz, undefaa, undefab, undefac, undefad, undefae, undefaf, undefag, undefah, undefai] 以及诸如 Aristotle [undefaj] 这样的交互环境，已将强化学习和语言模型深度整合到经过验证的数学与开源证明辅助工具中。与此同时，当前驱动商业聊天界面的推理扩展模型，已直接将强大的问题解决能力交到了数学家手中 [undefak, undefal, undefam, undefan, undefao]。

然而，对这些系统的亲身实践表明，数学研究中一个关键维度仍未得到充分支持：即如何将这些能力编排成一个长期、有状态、协作式的工作流程。日常的数学研究很少是一系列孤立的查询或计算机辅助证明；它涉及管理不确定性、综合梳理分散的文献、起草和修改中间产物，以及在数天或数周内追踪复杂、分叉的假设。

由于标准聊天界面本质上是临时性的，而专用引擎又缺乏更广泛的上下文，研究人员必须充当对话式头脑风暴、形式化证明器和计算脚本之间的人工连接纽带。尽管软件开发者越来越依赖AI驱动的编码环境来提供这种精确的编排能力，但这些工具从根本上是为代码的生命周期而优化的，而非数学领域独特的抽象概念、证明和工件。为了真正加速发现，我们认为AI辅助数学的下一阶段必须聚焦于这一缺失的编排维度，原生支持数学活动中完整、混乱的现实形态。

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

为了建立数学领域这一缺失的智能体工作流，我们引入了AI合作数学家——这是一个工作台，让数学家能够基于最新的Gemini语言模型，交互式地利用AI智能体进行开放式研究探索。

AI 数学协作者提供了一个有状态的交互式工作空间，其中项目协调员智能体将复杂任务委派到多个并行工作流中，使用户能够引导并参与不断演进的研究过程，而非等待端到端的自主执行。与其他智能体系统一样，AI 数学协作者是一个设计用于配合标准商用语言模型的框架，不依赖任何自定义模型行为或训练。这一架构方向与近期实证领域构建专用多智能体工作台（针对开放式假设生成和科学数据分析进行优化）的趋势相呼应 [undefao, undefas]。

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

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

2 AI辅助数学的设计原则

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

拥抱超越证明的数学：

真正的数学发现涉及一系列远超定理证明的复杂活动，例如迭代优化研究问题、梳理文献、头脑风暴，以及进行大量计算和数值模拟以建立直觉，仅举几例。[undefau] 认为，将数学简化为孤立的逻辑形式主义忽略了该学科深刻的准经验现实，而我们的设计有意反映并支持这种整体性的、多模态的现实，而非仅仅以最终的定理证明为索引。

支持意图的迭代优化：

在许多领域，用户从一开始就确切知道自己想要什么。然而在数学中，发现过程高度依赖于持续的迭代与优化。正如[undef]在其关于合情推理的研究中所展示的，提出正确的问题往往需要大量的启发式试错才能起步。正如格奥尔格·康托尔所言：“在数学中，提出问题的艺术必须被认为比解决问题更有价值”[undefav, 第27页]。像AlphaEvolve这类系统的经验也证实了这一点：数学家们会花费大量精力主动迭代，以确定究竟该聚焦于哪个问题——在扩大规模之前，先通过小规模运行或相关问题进行测试[undefq, undefr]。我们设计了一个灵活的界面，支持多种探索路径，使用户能够流畅地优化定义、问题和猜想。

生成原生的数学产物：

数学研究者已经拥有标准化的研究工作流程。不同于输出转瞬即逝的聊天记录或过早打磨成型的文稿，AI 数学协作者将其工作流程围绕一份“活的工作论文”展开。在传统工作流程中，起草和批注能帮助数学家构建起关于项目的严谨心智模型——清楚知道哪些部分已经稳固，哪些部分需要进一步关注。由于自主推理系统可以在幕后异步完成大量这类探索性工作，用户面临失去这种有机上下文的风险。为了帮助用户重建其心智模型，我们的系统会追踪研究的演变状态，并通过内联文本和页边注释将其可视化。通过明确提供上下文——例如特定论断的来源或某个草稿引理存在争议的程度——系统以一种完全符合数学界习惯的格式，将 AI 的底层过程呈现出来。

支持异步交互与灵活引导：

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

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

通过渐进式披露管理认知负荷：

当用户与多个 AI 智能体协作探索多条并行路径、从死胡同回溯并复用中间结果时，复杂研究会变得难以驾驭。如果高层策略（例如“尝试不动点方法”）与多个后台智能体的底层执行日志（例如“我们必须验证第 40 行的可测性”）混杂在一起，一段冗长且无结构的对话很快就会变得不可用。为了控制向数学家展示的信息量，我们的协作界面采用了渐进式披露策略，通过镜像智能体自身的层级结构，将高层意图与底层执行区分开来。默认情况下，用户主要与项目协调智能体交互，该智能体会过滤掉专业智能体沙盒中低层执行的嘈杂信息。然而，系统始终允许用户按需深入查看任何并行智能体活动的细粒度细节。

追踪、管理并沟通不确定性：

数学发现对严谨性有着极高的要求，一个存在缺陷的引理或虚构的参考文献就可能毁掉整篇论文。由于基础模型的推理能力容易出现难以预料的缺陷，其零样本输出会在一个要求精确的领域中引入不确定性的基线。该系统的架构并非试图隐藏这种摩擦，而是围绕这种不确定性的生命周期进行设计。它通过维护详细的版本历史来追踪不确定性，这主要用于让智能体（同时也对用户开放）监控论断如何演变或受到质疑；它通过用算力换取验证来管理不确定性（例如，通过持续审查、数值模拟和系统化的引文检查）；并且，它通过识别审查过程在论证的特定部分停滞不前来沟通这种摩擦。系统利用内联高亮和边注来吸引用户对这些停滞部分的注意，从而突出工作论文中需要人类更仔细审视的区域。通过将不确定性视为一个需要被编排的核心变量，而非一个简单的错误状态，该系统能够从本质上不可预测的模型中综合出稳健的数学输出。

保留失败探索的历史记录：

在数学研究中，知道什么行不通往往与知道什么行得通同样重要。虽然智能体被配置为绕过障碍，但系统承认特定的目标或并行工作流可能会以失败告终。该架构不会默默地重新开始或清除这些不成功尝试的历史，而是将死胡同视为第一等的、永久性的结果。保留项目历史中的这种“负面空间”对于攻克困难的数学问题至关重要。通过维护失败目标和已穷尽策略的持久记录，系统为用户和AI提供了背景信息，使他们能够基于这些失败共同制定出新的、信息更充分的工作流，这反映了“反驳是数学进步的基础”这一观点[undefa]。

3 实践中的人工智能合作数学家：操作演示

为了展示我们的设计原则如何在实践中体现，我们以协同数学家原型的一次代表性会话为例进行说明。

在该场景中，一位数学家探索计算几何领域的一个开放性问题：证明能够绕过左旋和右旋直角转角的"沙发"面积的上界。这是[undefaw]首次提出的问题的一个变体，其下界在近期将AlphaEvolve应用于数学优化问题的研究[undefax]中有所探讨。

该系统并非作为标准对话式聊天机器人运行，而是提供一个关联的"工作空间"，用于存储项目的所有信息。该工作空间由一组分层级运作的智能体操作，这些智能体将工作成果写入共享文件系统，并通过内部消息系统进行通信。用户提供输入并与顶层项目协调智能体讨论想法，该智能体再将任务委派给链条下游的其他智能体，以此类推。与人类组织类似，我们观察到，为智能体提供沟通渠道和清晰的升级路径，以便它们在遇到问题时使用，对于团队运作至关重要。智能体组织架构的示意图见图1。

3.1 初步探索

标准的零样本大语言模型要求用户预先加载一个完美的提示词。为体现我们支持意图迭代优化的原则，AI协同数学家首先进入一个交互式引导阶段，旨在帮助用户将意图形式化。

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

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

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

3.2 分支研究

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

这里我们描述了一个场景，其中项目协调智能体为每个目标启动一个工作流，但也可以为每个目标定义多个工作流，或者让某些目标暂时没有工作流，直到它们所依赖的工作完成。

目标1：文献综述：一个工作流协调智能体将任务委派给专门的文献综述子智能体。该子智能体利用我们计算密集型的搜索工具，发现了包含解决沙发问题先前上界所用机制的关键论文。在获得重要参考文献的指引后，它使用特定的网页和文献访问工具直接查询这些文献，以确定关键结果的确切表述和证明过程。

目标2：计算框架：另一个工作流协调智能体负责设计所需的计算框架。基于先前文献中观察到的策略，该工作流协调智能体首先设计计算框架的高级逻辑，使用子智能体创建工具派遣 Gemini Deep Think 来证明这能够给出所需的严格上界。一旦证明完成，它再使用另一个子智能体创建工具创建一个编码智能体，指示其实现所需的 Python 库，并附带相关测试和演示案例。当每个智能体给出状态更新时，工作流协调智能体会异步更新面向用户的工作流报告，详细说明证明过程，并提供关键代码文件的链接。

现有系统中的所有证明都是纯粹非形式化的，但增加像 AlphaProof 这样的形式化证明器，将有可能提高对证明正确性的信心——前提是这些证明能够利用现有的形式化数学库进行表述和验证。或者，使用像 Aletheia 这样更强的非形式化证明系统，将为系统增加相当大的能力，但也会带来相应的计算成本。

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

在当前原型中，此类计算搜索是通过标准智能体原语的组合来执行的，但加入诸如 AlphaEvolve 之类的进化搜索算法，将为这类优化和搜索流程提供强大的加速引擎。

3.3 交互式引导与硬约束

当被要求解决困难的研究问题时，标准 AI 智能体常常会找到无效的捷径、编造引理、对细节含糊其辞，并过早地宣称成功。AI 合作数学家的一项关键技术特征在于应用硬性程序约束来防止这些失败模式，并结合用户主动的人工引导。

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

项目协调智能体在被迫管理和披露自身不确定性时，会向用户发出警报，并在聊天中明确请求帮助：“我们最初实现的搜索效率不足以找到所需结果，且文献中可参考的类似案例也不多。您是否有数学直觉，能提供一种更好的剪枝策略？当前方法的更多细节可参见以下文档。”

关键在于，智能体工作时用户不会被锁定。通过聊天界面，用户阅读项目协调智能体的更新，并主动引导项目进展：发送消息建议采用拓扑剪枝启发式方法，同时指示协调智能体在当前工作继续进行的过程中，创建额外的工作流来研究新的边界策略。

3.4 最终输出

在用户引导系统突破计算瓶颈后，各工作流完成其特定目标。然而，最终输出并非短暂的聊天消息。每个工作流协调智能体的主要输出是一份经过编译和审阅的 LaTeX 文档，当用户打开该工作流时，这份文档会醒目地展示出来。

为了生成自然的数学成果，我们要求协调智能体在这些文档中满足特定标准：

阐述：

草稿必须包含对研究过程（即如何得出该结果）的说明，而不仅仅是最终结果。

边注：

文档利用边注提供额外信息，明确将结论与工作空间关联起来。例如，一条边注可能写道：[剪枝启发式方法源自用户建议；基线边界值 2.2195 来源于 arxiv.org/abs/… 上的论文]。

内部链接：

除了外部文献，文档还会引用智能体创建的内部文档，为用户提供直接入口，以便审计共享文件系统。

审阅流程：

在报告被标记为定稿并完成工作流之前，报告必须提交至论文审阅流程，由多位 AI 审稿智能体对其内容和风格进行严格审查，这些智能体均具备交叉验证参考文献、代码输出以及逻辑正确性的工具和能力。审稿智能体在每轮审阅之间持续存在，形成迭代过程，报告在此过程中不断被优化和改进，只有当所有审稿人正式批准报告后，该流程才会结束。为避免无限循环，若工作流协调智能体无法通过审阅流程，可将此问题上报给项目协调智能体。在此情况下，该工作流将被标记为未完成，并向用户清晰显示上报消息，使用户能立即了解该报告可能包含未解决的问题。

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

从历史上看，人工智能在数学领域的进展一直是通过静态问题求解基准来衡量的。如今，该领域严重依赖此类基准，包括 IMO ProofBench、FrontierMath 和 PutnamBench，而它们的先驱 MATH 和 GSM8K 在衡量早期大语言模型进展方面曾极具影响力。

然而，鉴于前沿系统在原始问题求解能力上已被证明达到或超过人类专家水平，我们认为提升这一能力的增量价值正在降低，而人工智能辅助数学的进展现在至少部分受制于其他能力，这些能力反映了专业数学家更广泛的工作流程。类似的评估转变也正在其他科学领域出现，即通过直接运行湿实验和解决未解决问题来衡量现实世界的成功。

这意味着，首先，AI 系统应针对更广泛的任务进行衡量。诸如用于通用事实查找的 DeepSearchQA [undefaaf] 以及用于竞赛数学证明中错误查找的 Hard2Verify [undefaag] 等基准测试，所衡量的能力与数学研究过程中的能力具有精确的对应关系。但据我们所知，目前尚未针对专业数学研究场景开发出类似的基准测试。随着 AI 系统的改进，对这些辅助能力（及其改进！）的清晰衡量将变得越来越重要，以减轻“锯齿状前沿”[undefaah] 的严重性，以及由此带来的人类驱动数学与 AI 驱动数学之间的阻抗不匹配问题。

然而更重要的是，我们认为，用于数学的 AI 系统默认应被视为人在回路的系统，其进步和成就也应据此衡量。这呼应了我们的设计原则：我们系统的首要目的是协助数学家完成工作，而非独立于他们取得成功。基于这一框架，我们首先展示由数学家直接使用 AI 合作数学家所产生的结果（第 5 节），随后是对 AI 合作数学家静态问题解决能力的衡量（第 6 节）。

5 与数学家的初步成果

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

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

5.1 案例研究：一个库罗夫卡问题

早期用户 M. Lackenby 使用 AI 协同数学家研究了拓扑学和群论中的几个问题。他的工作解决了一个开放性问题（库罗夫卡笔记中的问题 21.10）。该问题询问是否每个有限群都允许一个所谓的“恰好有限表示”，即一个有限表示，其中删除任何关系都会导致一个无限群。结果答案是肯定的。Lackenby 在此案例中的过程，体现了“数学家参与其中”式交互的价值。

拉肯比首先直接输入了问题陈述；系统确认了含义，随后创建了两个独立的工作流，一个试图证明该结论，另一个则试图证伪它。最先返回的结果是一个系统自身标记为错误的“证明”——某个工作流撰写了一个论证，但随后一个评审智能体发现了其中的缺陷。然而，当拉肯比查看论文时，他意识到尽管存在这个漏洞，但其中包含了他称之为“非常非常巧妙的证明策略”。此外，当他阅读评审对该证明的批评意见时，他意识到：“等等，我知道怎么填补这个漏洞了。”

他指出了一种修正该论证的方法，系统随后能够撰写出一份完整且正确的证明。最后，拉肯比下载了文档，应用了自己的修订——对结论进行了泛化并添加了示例——然后再次上传，并要求项目协调员创建一个用于最终审查的工作流。系统照做了，在论文中发现了两个小问题，他针对最终版本进行了修正。

从这个案例中得到的教训是，人工智能与数学家之间的反复交流对于问题的解决至关重要。在拉肯比看来，这表明“当用户熟悉该领域时，系统运行效果最佳。”虽然有人可能将此视为一种局限，但他补充道：“让它解决一个我完全不懂的问题，又有什么意义呢？”

智能体操作

在幕后，该工作流的协调智能体：

• •

  创建了一个编码子智能体，用于对非恰好有限表示进行计算搜索，并成功找到了两个示例。

• •

  对这些示例进行了分析，并进行了文献检索，以识别与其构造相关的理论，从而得出了一种生成非恰好有限表示的通用方法。

• •

  注意到这并未否定性地解决该猜想（因为一个群可能有多种表示，找到一个非恰好有限表示并不意味着所有表示都不是恰好有限的），但决定基于这一论证在此处结束其工作流，并提出了一个更精确的猜想，随后将报告发送以供审查。

• •

  在审稿流程中，与审稿智能体展开了一场来回讨论。在此过程中，其中一位审稿智能体发现了一种可用于从正面证明该猜想的方法。

• •

  与审稿人达成一致后，将工作流转向撰写该方法。经过进一步审阅，由此形成的草稿经 Lackenby 补充完善，最终完成了证明。

5.2 案例研究：斯特林系数

另一位早期用户 G. Bérczi 在与 AI 数学合作者合作时，首先着手解决一个关于对称幂表示中斯特林系数行为的问题。具体而言，该猜想假设在某个二项式展开中，系数不仅严格为正，而且构成一个对数凹序列。

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

针对 Bérczi 提出的问题，这位 AI 合作数学家分别在独立工作流中为其中两个猜想建立了证明（目前正在接受详细的人工审核）。此外，它还为其主张以及针对未证明猜想的研究提供了详细的计算证据。Bérczi 指出，该系统的设计在多个方面提供了帮助。不仅很容易通过“绿色勾号”追踪已完成的任务，更重要的是，最终文档中的一条边注提示了他一个关键洞见，他得以通过聊天界面就此进行提问。尽管如此，他指出与 AI 系统协作需要一定的技巧，并表示“现在要掌握它的用法并非易事”，同时认为“这将导致数学家之间因使用这些模型的方式不同而产生巨大差异。”

智能体操作

两个关键工作流提供了这些猜想的声称证明。为说明工作流程，在第一个工作流中，协调智能体：

• •

  创建了一个编码子智能体，对展开式进行初步的计算枚举，枚举范围控制在几分钟内可合理运行的程度。

• •

  从结果中观察到，该猜想在 情况下不成立，但在 较大时似乎成立，并且其原有的证明策略是无效的。

• •

  使用 Gemini Deep Think 子智能体为修正后的猜想提出新的证明策略。它成功做到了这一点，说服了工作流协调智能体，随后也说服了审核智能体。

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

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

通过该系统，Rezchikov 与项目协调智能体讨论了问题，并提供了包含与问题陈述相关结果的补充论文，直到就任务的精确定义达成一致，并创建了一个工作流来尝试解决该问题。该工作流生成的报告包含一个关键引理及其优雅的证明，该证明经仔细核查后成立，并基本解决了 Rezchikov 提出的问题。Rezchikov 还指出，其他 AI 系统在收到相同提示词时未能证明该结果，不过由于缺乏多次采样尝试和受控条件，很难从这类单次实验中得出结论。

Rezchikov 还提出了另外两点观察，揭示了该系统的价值。其一涉及对一种似乎无效的方法的探索：其附加价值在于，该系统让他比平时更快地走到了死胡同。正如他所说：“我本可以轻松花上一周时间幻想那里有什么，但相反，我直接继续前进了。”此外，他指出正确证明的质量相对较高：“从美学角度，我会将其证明的总体风格评为我用过的所有模型中最好的。”

这展示了 AI 数学协作者如何以自然融入研究人员典型探索性研究工作流程的方式，帮助数学研究者探索想法。

智能体行动

在此案例中，工作流协调智能体：

• •

  使用专用工具进行了文献综述，研究了针对该问题的常用技术和常见陷阱，从而突出了除 Rezchikov 提供的要点之外还需注意的几个关键特性。

• •

  进行了具体的后续文献查询，以理解这些要点的确切性质。

• •

  将问题陈述和关键上下文信息传递给 Gemini Deep Think，后者生成了证明（包括关键引理），随后该证明被整理成报告。

6 问题求解基准测试结果

在论证了更广泛能力测量的必要性之后，我们承认，问题求解基准是目前衡量人工智能系统在数学领域表现的最佳客观指标。在本节中，我们将讨论我们尝试使用此类基准来测量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 数学协作者成功地将该问题的核心简化为一个布尔可满足性（SAT）问题，并使用 PySAT 库对其求解。为了使这种框架成立，需要对核心问题进行若干非平凡的调整——这种解决方案显然有利于拥有持久文件系统和智能体代码编写能力的系统。虽然其他模型的评估框架允许执行代码，但开发和测试更复杂的库对它们来说很难实现。Gemini 3.1 Pro 和 Gemini Deep Think 都试图对该问题采用纯理论解法，而在这个案例中，这要困难得多。

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

在一个兼具理论与计算双重性质的组合数学问题中，我们看到这位 AI 数学协作者将其工作清晰地划分为多个工作流，分别对解题的理论基础进行完善，以及独立开发代码。在理论工作流中，进行抽查的评审员指出了多处逻辑错误与不一致之处（与其他模型所犯的错误类似），这些错误最终在最终工作流报告中得到了修正，使得项目协调员能够将各个部分整齐地整合起来，得出正确的解答。

6.2 FrontierMath

一个自然的比较对象是外部的 FrontierMath 基准测试 [undefaz]。Epoch AI 在该基准测试的第 4 层级上，以上述的“最终答案”模式对 AI 数学协作者进行了测试。用 Epoch AI 的话来说，“这个极端层级包含 50 个由教授和博士后设计、作为短期研究项目的问题。其难度旨在超越第 3 层级，其中一些问题可能在未来数十年内仍无法被 AI 解决。”来自所有主要提供商的前沿模型和系统都会定期在 FrontierMath 基准测试上进行测试。222 最新结果和排行榜可查看 https://epoch.ai/frontiermath/tiers-1-4?tier=Tier+4。

评估以盲测方式进行，Epoch AI 直接访问 AI 数学协作者的界面，自行输入问题并获取答案，系统开发者在此过程中既未看到问题，也未观察到评估期间项目工作区的状态。

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

与先前评估的一个重要区别在于，FrontierMath 评估通常使用由 Epoch AI 开发的标准智能体框架来执行。一个显著的例外是：Gemini 2.5 Deep Think 也通过网页界面进行了评估，未使用额外框架。这种方式提供了 Python 解释器的访问权限，但也对智能体运行轨迹中使用的 token 数量设置了硬性限制（在相关模型 API 中会对此进行核算）。然而，在我们的设置中，我们仅使用自己的工具实现，并且对模型调用次数或生成的 token 数量不设限制。这意味着我们的系统可能比先前评估的系统具有更高的推理成本。

7 挑战与局限

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

讨好评审者的偏见（虚假共识）：

迭代审阅过程是一个动态系统，它不断演化着工作文档。当某个智能体提出了一个它自身无法真正修正的有缺陷论点时，满足审阅智能体的严格约束有时会导致该系统收敛于一个仍然存在缺陷的论点，但其中的错误已无法被审阅智能体检测到。这类论点对人类来说也可能难以厘清，这已被强调为当前 AI 系统的一个局限性 [undefaaj]。文献中已注意到证明者-验证者动态中类似的病理现象 [undefaak]。尽管这种行为相对罕见，但它违反了我们在核心原则上明确承认不确定性的要求。

无法解决的分歧（非终止）：

相反，当迭代审阅过程未能达成共识时，它可能完全无法终止。在这种动态下，迭代审阅过程会陷入无休止的修订与拒绝循环中。在连续的自主迭代中，这种循环往往会退化为日益严重的幻觉推理——一种俗称“死亡螺旋”的现象。尽管我们已实施各种机制来缓解这些影响，但语言模型之间频繁相互争执的核心问题依然存在。早期用户已注意到这种行为，学会了识别工作流何时进入这种状态，并相应地降低对其输出的信任度。

系统自主性需要让渡控制权：

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

表征的语义含义：

我们的团队很早就认识到，数学家往往倾向于将排版精美的文档与相应严谨的内容质量联系起来，而大语言模型却恰恰违背了这种直觉——它们擅长生成完美的 LaTeX 格式，却常常在严格的逻辑验证上挣扎。在 AI 合作数学家中，我们试图通过将输出标记为带有旁注的“工作文档”来缓解这一问题，但似乎可以开发新的界面来更直观地呈现此类文档的特征。近期人机交互领域由 AI 赋能的研究（例如，[undefaal]）或许能为未来的发展方向提供灵感。

此外，将高度能干的智能体系统引入数学生态系统也伴随着一定风险。展望未来，该社区必须应对若干系统性挑战：

维持文献中的信噪比：

随着 AI 系统在 LaTeX 排版和文献综合方面变得高度熟练，社区将需要应对潜在的自动化输出激增。如果这些工具被频繁用作自主生成器，而非人类引导的协作者，该领域将出现更多看似合理但浅薄、增量式或存在细微缺陷的论文。这种转变可能会增加系统性的“语义噪声”，迫使研究人员开发新的启发式方法，以便在更高基数的稿件中高效识别真正新颖的数学发现。形式化方法和自动形式化可能有助于检查论文的正确性并突出其中的缺陷，但无法替代社区成员理解并吸收新发表成果内涵的过程。

调整同行评审生态系统：

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

8 结论

AI 社区近期已跨越多个技术里程碑，在各类数学基准测试中展现出人类级和超人类的表现。然而，若想真正加速科学发现，解决静态且定义明确的问题只是其中一环。数学研究的前沿并非线性的对话或一系列互不关联的谜题；它是一个混乱、重叠、高度迭代的过程，其特点在于未经证明的直觉、分支假设以及复杂的人类协作。

AI 合作数学家旨在契合研究人员的实际工作方式。该系统并非将 AI 简化为一个孤立的预言机或简单的验证流水线，而是作为一个整体性的工作空间。通过管理不确定性的生命周期、通过层级委派来模拟人类工作流程，并将其输出扎根于原生数学产物，该系统将强大的基础模型提升为自然的协作者。借助严格的程序化约束以及对一份动态“工作论文”的持续维护，系统确保整个研究历程——失败的测试、综合的文献、以及思想的持续精炼——都被捕获、审计，并明确传达给用户。正如早期用户解决开放问题并发现新颖证明所展示的那样，这种双向交流使人类能够有效地引导 AI 突破困难瓶颈。

然而，要实现这一范式的全部潜力，需要 AI 社区转变衡量成功的方式。尽管这些基准测试在评估模型针对精心设计的问题生成最终答案的能力方面表现出色，但它们并未涵盖前沿研究的全部范畴。它们并非为衡量系统交互式修剪假设树、综合小众文献，或在扩展失败时适当暂停并披露不确定性的能力而设计。

如果我们想要构建能够充当真正合作数学家的系统，就必须开发互补的评估框架，用以衡量协作效能、有状态的探索过程以及对不确定性的严格管理。AI 辅助数学的下一次革命，将不仅仅由哪个模型能最快合成正确答案来定义，更取决于哪个系统能最有效地帮助人类研究人员在未知领域中导航。

致谢

我们要感谢：

Edward Lockhart、Allison Woodruff、Juanita Bawagan、Uchechi Okereke、Thang Luong 对本报告的审阅。

Anna Trostanetski、Andrey Petrov、Matin Akhlaghinia、Victoria Johnston、Nick Dietrich 在改进原型系统的部署设置和可靠性方面提供的帮助。

Mariana Felix、Francesca Pietra 在外部化和合作伙伴关系方面提供的建议。

Uchechi Okereke、Gemma Gibbs 提供的法律咨询。

Adriana Lara、Armin Senoner、Danielle Breen、Duncan Smith、Juanita Bawagan 在沟通策略和命名方面提供的建议。

Henryk Michalewski 对研究数学问题内部数据集的维护。

Greg Burnham（Epoch AI）对 FrontierMath 评估的协调。

Ellen Jiang 在用户界面建议和改进方面提供的帮助。

Victoria Johnston、Doug Fritz、Felix Riedel 对前端代码的审查。

Sébastien Racaniere、Romu Elie 与早期测试者及数学界成员沟通，并反馈他们的见解和需求。

Richard Bamler、Johannes Bausch、Mehdi Bennani、Gergely Bérczi、David Berghaus、Otis Chodosh、Bennett Chow、Maria Chudnovsky、Romu Elie、Sergey Galkin、Javier Gómez-Serrano、Matt Harvey、Amaury Hayat、Marcus Hutter、Ray Jiang、Ayush Khaitan、Alex Kontorovich、Robin Kothari、Marc Lackenby、Tor Lattimore、Igor Makhlin、Johan Martens、Alex Matthews、Stanislav Nikolov、Georg Ostrovski、Stan Palasek、Sébastien Racaniere、Danylo Radchenko、Johannes Ruf、Julian Salazar、Simone Severini、Phiala Shanahan、Iain Smears、Elahe Vedadi、Adam Zsolt Wagner，感谢他们测试系统并提供反馈。

Javier Gómez-Serrano 和 Terence Tao 对文献搜索功能的早期测试和反馈。

感谢 Nada Baessa、Bruno Vergara Biggio、Semon Rezchikov 在深度测试、输出结果检查、详细反馈和功能需求方面提供的帮助。

感谢 Allison Woodruff、Patrick Gage Kelley 在协助访谈早期用户和整理反馈方面提供的帮助。

感谢 Marc Lackenby 在系统数学性能反馈、工作流与界面设计输入以及深度数学协作方面提供的帮助。

感谢 JD Velasquez、Yunhan Xu 在分发和产品视角方面提供的建议。

感谢 Victor Martin、Stig Petersen、Petko Yotov、Hamish Tomlinson、Sam Blackwell 在获取算力和协助模型服务方面提供的帮助。

感谢 Sam Blackwell 在工程支持和建议方面提供的帮助。

感谢 Stig Petersen 在技术审阅方面提供的帮助。

感谢普林斯顿高等研究院（IAS）去年主办了一场联合研讨会，其中讨论了许多相关议题。

在本手稿的撰写过程中，我们在多个阶段使用了 Gemini 3.1 Pro，用于起草正文的部分内容、校对人工撰写的章节，以及制作和迭代图表。

贡献者

Y.Z. 设计了系统的初始原型。Y.Z.、I.V.G.、D.Z.、I.B.、L.B.、A.D. 继续开发了核心系统和用户界面，并开展了提升能力的研究，V.K. 提供了研究思路方面的意见。M.W.、D.K. 在整个原型迭代过程中提供了意见和测试。M.W. 设计了用户界面和工作流的关键元素，F.V. 设计了视觉语言及其他 UI 元素。T.S. 开发了外部用户访问系统的路径。S.A. 制定了系统对外输出的需求。I.V.G.、Y.Z.、D.Z.、I.B.、L.B.、A.C.、T.S. 为外部用户维护了系统。Y.Z.、I.V.G.、D.Z.、I.B.、L.B.、D.M.R.、H.M. 准备了系统的内部和外部评估。D.M.R.、M.W.、D.Z. 撰写了论文，I.V.G.、Y.Z.、A.D.、B.G.、F.V. 提供了意见。F.V.、M.W.、D.Z.、D.M.R. 制作了图表。B.G. 协调了外部用户社区。D.Z.、I.V.G. 和 G.H. 协调了团队。A.D. 和 D.Z. 制定了整体策略。A.D. 和 P.K. 监督了研究项目。

参考文献

• 乔治·波利亚《数学中的归纳与类比：数学与合情推理第一卷》，普林斯顿大学出版社，1954 年
• 伊·拉卡托斯《证明与反驳：数学发现的逻辑》，剑桥大学出版社，1976 年
• D. 爱泼斯坦、S. 莱维和 R. 利亚韦《关于本刊》，载于《实验数学》第 1 卷第 1 期，1992 年
• Aitor Lewkowycz 等人《利用语言模型解决定量推理问题》，2022 年，arXiv:2206.14858
• Ross Taylor 等人《Galactica：面向科学的大语言模型》，2022 年，arXiv:2211.09085
• Zhangir Azerbayev 等人《Llemma：一个开放数学语言模型》，载于国际学习表征会议 (ICLR)，2024 年，arXiv:2310.10631
• Xiang Yue 等人《MAmmoTH：通过混合指令微调构建数学通才模型》，载于国际学习表征会议 (ICLR)，2024 年，arXiv:2309.05653
• 邵志宏等人《DeepSeekMath：突破开放语言模型数学推理的极限》，2024 年，arXiv:2402.03300
• Mistral AI《Mathstral 7B》，https://huggingface.co/mistralai/mathstral-7B-v0.1，2024 年
• 杨安等人《Qwen2.5-Math 技术报告：通过自我改进迈向数学专家模型》，2024 年，arXiv:2409.12122
• Chris Lu 等人《AI 科学家：迈向全自动开放式科学发现》，2024 年，arXiv:2408.06292
• Thang Luong 和 Vahab Mirrokni《利用 Gemini Deep Think 加速数学与科学发现》，https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/，2025 年
• 何巨杰等人《Skywork Open Reasoner 1 技术报告》，2025 年，arXiv:2505.22312
• Yutaro Yamada 等人《AI 科学家 v2：通过智能体树搜索实现工作坊级别的自动化科学发现》，2025 年，arXiv:2504.08066
• 刘刚、朱一涵、陈杰和蒋萌《通过深度研究增强 AlphaEvolve 实现科学算法发现》，载于国际学习表征会议 (ICLR)，2026 年，arXiv:2510.06056
• [undefo] Max Zimmer、Nico Pelleriti、Christophe Roux 和 Sebastian Pokutta 著《智能体研究员：数学与机器学习中 AI 辅助研究实用指南》，2026 年，arXiv:2603.15914
• [undefp] Tony Feng 等人著《迈向自主数学研究》，2026 年，arXiv:2602.10177
• [undefq] Bernardino Romera-Paredes 等人著《利用大语言模型进行程序搜索的数学发现》，载于《自然》第 625 卷，2024 年，第 468–475 页，DOI: 10.1038/s41586-023-06924-6
• [undefr] Alexander Novikov 等人著《AlphaEvolve：面向科学与算法发现的编码智能体》，2025 年，arXiv:2506.13131
• [undefs] Mert Cemri 等人著《AdaEvolve：自适应 LLM 驱动的零阶优化》，2026 年，arXiv:2602.20133
• [undeft] Asankhaya Sharma 著《OpenEvolve：一个开源进化式编码智能体》，GitHub，2025 年，URL: https://github.com/algorithmicsuperintelligence/openevolve
• [undefu] Robert Tjarko Lange、Yuki Imajuku 和 Edoardo Cetin 著《ShinkaEvolve：迈向开放且样本高效的程序进化》，载于《国际学习表征会议（ICLR）》，2026 年，arXiv:2509.19349
• [undefv] Thomas Hubert 等人著《利用强化学习进行奥林匹克级别的形式化数学推理》，载于《自然》，2025 年，DOI: 10.1038/s41586-025-09833-y
• [undefw] Peiyang Song、Kaiyu Yang 和 Anima Anandkumar 著《Lean Copilot：在 Lean 中原生运行 LLM 推理的框架》，2024 年，arXiv:2404.12534
• [undefx] Haiming Wang 等人著《LEGO-Prover：利用不断增长的库进行神经定理证明》，载于《国际学习表征会议（ICLR）》，2024 年
• [undefy] Z. Ren 等人著《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式化数学推理》，2025 年，arXiv:2504.21801
• [undefz] Yong Lin 等人著《Goedel-Prover-V2：利用脚手架数据合成与自我修正扩展形式化定理证明》，载于《国际学习表征会议（ICLR）》，2026 年，arXiv:2508.03613
• [undefaa] Zenan Li 等人著《通过协同 LLM 与符号推理证明奥林匹克不等式》，载于《国际学习表征会议（ICLR）》，2025 年
• [undefab] 陈江杰等人著《Seed-Prover 1.5：通过经验学习掌握本科级别定理证明》，2025年，arXiv:2512.17260
• [undefac] 王海明等人著《Kimina-Prover Preview：迈向基于强化学习的大型形式化推理模型》，2025年，arXiv:2504.11354
• [undefad] Sidharth Hariharan 等人著《形式化的里程碑：八维空间中的球体堆积问题》，2026年，arXiv:2604.23468
• [undefae] 李阳等人著《HunyuanProver：面向自动定理证明的可扩展数据合成框架与引导式树搜索》，2024年，arXiv:2412.20735
• [undefaf] Prithwish Jana 等人著《ProofBridge：通过联合嵌入实现自然语言证明到 Lean 的自动形式化》，发表于国际学习表征大会（ICLR），2025年
• [undefag] 陈大伟等人著《亏格零与一中 -微分形式的奇偶性》，2026年，arXiv:2602.03722
• [undefah] 刘俊奇等人著《Numina-Lean-Agent：面向形式化数学的开放通用智能体推理系统》，2026年，arXiv:2601.14027
• [undefai] Marco Del Tredici 等人著《Ax-Prover：基于大语言模型与 MCP 验证器的智能体 LEAN 证明》，ICLR 2026 会议桌面拒稿/预印本，2025年
• [undefaj] Tudor Achim 等人著《Aristotle：国际数学奥林匹克级别的自动定理证明》，2025年，arXiv:2510.01346
• [undefak] David P. Woodruff 等人著《利用 Gemini 加速科学研究：案例研究与通用技术》，2026年，arXiv:2602.03837
• [undefal] Sébastien Bubeck 等人著《GPT-5 的早期科学加速实验》，2025年，arXiv:2511.16072
• [undefam] Boris Alexeev 等人著《组合学与数论中的简短证明》，2026年，arXiv:2603.29961
• [undefan] Boris Alexeev 等人著《组合学、概率论与数论中的简短证明（二）》，2026年，arXiv:2604.06609
• [undefao] Juraj Gottweis 等人著《迈向人工智能协同科学家》，2025年，arXiv:2502.18864
• [undefap] Google 著《Google 反重力》，访问日期：2026-04-27，https://antigravity.google/，2025年
• [undefaq] Anthropic 著《Claude Code》，访问日期：2026-04-27，https://www.anthropic.com/product/claude-code，2025年
• [undefar] OpenAI 著《OpenAI Codex》，访问日期：2026-04-27，https://openai.com/index/introducing-codex/，2021年
• [undefas] Ludovico Mitchener 等人。“Kosmos：用于自主发现的人工智能科学家”，2025 年，arXiv:2511.02824
• [undefat] William P. Thurston。“论证明与数学的进展”，载于《美国数学学会公报》第 30 卷第 2 期，1994 年，第 161–177 页，DOI: 10.1090/S0273-0979-1994-00502-6
• [undefau] Hilary Putnam。“什么是数学真理？”，载于《数学、物质与方法：哲学论文集，第一卷》，剑桥大学出版社，1975 年，第 60–78 页
• [undefav] Joseph Warren Dauben。《格奥尔格·康托尔：他的数学与无穷哲学》，哈佛大学出版社，1979 年
• [undefaw] Leo Moser。“通过走廊搬运家具”，载于《SIAM 评论》第 8 卷第 3 期，工业与应用数学学会，1966 年，第 381 页
• [undefax] Bogdan Georgiev、Javier Gómez-Serrano、Terence Tao 和 Adam Zsolt Wagner。“大规模数学探索与发现”，2025 年，arXiv:2511.02864
• [undefay] Thang Luong 等人。“迈向稳健的数学推理”，载于《2025 年自然语言处理实证方法会议论文集》，2025 年，arXiv:2511.01846
• [undefaz] Elliot Glazer 等人。“FrontierMath：评估 AI 高级数学推理能力的基准”，2024 年，arXiv:2411.04872
• [undefaaa] George Tsoukalas 等人。“PutnamBench：在普特南数学竞赛上评估神经定理证明器”，2024 年，arXiv:2407.11214
• [undefaab] Dan Hendrycks 等人。“使用 MATH 数据集衡量数学问题解决能力”，载于《神经信息处理系统进展》第 34 卷，2021 年，第 29157–29169 页
• [undefaac] Karl Cobbe 等人。“训练验证器解决数学文字题”，2021 年，arXiv:2110.14168
• [undefaad] Thang Luong 和 Edward Lockhart。“配备 Deep Think 的 Gemini 高级版本正式达到国际数学奥林匹克金牌标准”，Google DeepMind 博客，Google DeepMind，https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/，2025 年
• [undefaae] Mohammed Abouzaid 等人。“首次证明”，2026 年，arXiv:2602.05192
• [undefaaf] Nikita Gupta 等人。“DeepSearchQA：弥合深度研究智能体的全面性差距”，2026 年，arXiv:2601.20975
• [undefaag] Shrey Pandit 等人。“Hard2Verify：面向开放式前沿数学的步骤级验证基准”，2025 年，arXiv:2510.13744
• [undefaah] Fabrizio Dell’Acqua 等人。“驾驭锯齿状技术前沿：人工智能对知识工作者生产力与质量影响的现场实验证据”，载于《组织科学》第 37 卷第 2 期，INFORMS，2026 年，第 403–423 页，DOI: 10.1287/orsc.2025.21838
• [undefaai] undef Epoch AI。“评估 Gemini 2.5 Deep Think 的数学能力”，访问日期：2026-05-05，https://epoch.ai/blog/deep-think-math，2025 年
• [undefaaj] Alex Kontorovich。“未来数学的形态”，2025 年，arXiv:2510.15924
• [undefaak] Xingyu Dang 等人。“逃离认知之井：利用现成模型高效完成竞赛数学题”，2026 年，arXiv:2602.16793
• [undefaal] undef People + AI Research。“借助 Lumi，更聪明地阅读，而非更费力”，访问日期：2026-04-23，https://medium.com/people-ai-research/read-smarter-not-harder-with-lumi-6a1a8210ccc7，2025 年