这项由谷歌DeepMind主导开发的研究成果发布于2026年5月7日，以预印本形式挂载于arXiv平台，论文编号为arXiv:2605.06651。研究由来自谷歌DeepMind与谷歌的近二十位研究人员共同完成，通讯作者为Daniel Zheng与Pushmeet Kohli。

一、数学家的烦恼：不是不够聪明，而是缺少一个真正懂行的助手

数学研究是一项极其奇特的工作。外界看到的，往往是数学家在黑板上潇洒地写下几行公式，宣布证明了某个定理。但这幅画面背后藏着的真实日常，却更像是一个侦探在昏暗灯光下翻阅厚厚的案卷——翻出来的，十有八九是死路，偶尔才能拼出一条线索。

一位数学家真正的工作日是什么样的？他可能花上整个上午，把一个直觉性的猜想拆开来反复端详，发现它在某个特殊情况下完全不成立，于是推倒重来。他可能花上几天，在文献堆里找一篇二十年前的老论文，就为了确认某个引理的精确条件。他可能写满好几页草稿，最后发现逻辑链在第三步就断了。这些过程——试错、反驳、重新定义、文献追溯——才是数学研究的真实面貌，只是它们从来不出现在最终发表的论文里。

近年来，人工智能在数学领域的进步确实令人瞩目。能解奥数题的模型、能辅助写Lean形式化证明的系统、能自动搜索算法结构的进化框架，一个接一个涌现出来。但这些工具都有一个共同的局限：它们擅长"解一道题"，却不擅长"陪一位数学家做研究"。解一道题，有明确的问题输入和答案输出；而做研究，问题本身就在不断变化，思路在不断分叉，失败的记录和成功的记录同样重要。

谷歌DeepMind的研究团队正是看到了这个空白，开发了他们称之为"AI数学协作者"（AI co-mathematician）的系统。这不是一个更聪明的聊天机器人，而是一个专门为数学家的真实工作方式量身设计的"工作台"。它的目标不是取代数学家，而是像一位真正的研究伙伴那样，陪着数学家一起摸索、试错、讨论、推进。早期测试中，已经有数学家借助这个系统解决了公开悬案问题，发现了新的研究方向，并找到了被遗漏的文献线索。在FrontierMath这一极高难度的数学问题评测基准的第四等级（Tier 4）上，这个系统以48%的正确率创下了所有AI系统的新纪录。

二、为什么现有工具不够用：聊天机器人与数学研究之间的鸿沟

在理解这个系统之前，有必要先搞清楚，为什么数学家使用现有的AI工具（比如各种聊天大模型）会感到"差那么一点"。

最核心的问题是：聊天界面是一次性的、无记忆的、线性的。你问一个问题，它给一个答案，这条对话就结束了。下次你再回来，它不知道你之前在研究什么，不知道你上周试过哪些路子失败了，不知道你的核心问题在上一轮讨论后已经微调了措辞。每次对话都是全新的开始，而数学研究绝对不是全新开始的——它是一个连续数周甚至数月的迭代过程，每一步都建立在之前所有步骤的基础上，包括那些走错的步骤。

用一个日常比喻来说：现有的聊天AI就像是你每次遇到问题都去问不同的陌生人，每个陌生人都很聪明，但他们彼此不认识，也不了解你的完整情况，给出的建议往往各说各话、难以整合。而真正的研究伙伴，是那种在你旁边坐了三个月、见证了你所有尝试与失败的人。

软件工程领域已经解决了类似的问题。程序员有版本控制系统（记录所有历史改动），有持续集成测试（自动验证代码是否正确），有设计文档（让AI代理在长期执行任务时保持方向感）。这些工具构成了一套完整的"迭代探索脚手架"，让AI辅助软件开发变得真正高效。GitHub Copilot、Claude Code、Google Antigravity这类工具之所以能真正改变程序员的工作方式，正是因为它们嵌入了这套脚手架。

数学研究却几乎没有任何类似的自动化支撑。数学家的"版本控制"是草稿纸和备忘录，"持续测试"是自己反复检验逻辑，"设计文档"是脑海中的研究计划。谷歌DeepMind这个系统的核心抱负，就是为数学研究构建一套类似的脚手架——不是模仿软件工程的形式，而是提炼其精髓，以数学研究本身的语言和工作方式来实现。

三、七条设计原则：一个系统的灵魂

这个系统的研究团队在动手写一行代码之前，先花了相当多的精力思考数学研究的本质。他们提炼出了七条设计原则，这七条原则共同构成了整个系统的哲学基础。

第一条原则叫做"超越证明来拥抱数学"。哲学家希拉里·普特南曾经指出，把数学简化为纯粹的形式逻辑，是对数学"准经验性"本质的忽视。数学家的日常工作包括提炼研究问题、梳理文献、头脑风暴、运行大量数值模拟来建立直觉等等，这些活动构成了研究的主体，而最终的形式证明只是其中一个环节。这个系统从一开始就被设计为支持所有这些活动，而不是单纯聚焦在"证明某定理"这一个任务上。

第二条原则是"支持意图的迭代精化"。数学家通常在项目开始时并不清楚自己确切想做什么，问题的精确表述本身就是研究的一部分。格奥尔格·康托尔的那句名言说得很清楚："在数学中，提出一个问题的艺术比解答它更有价值。"这个系统被设计为一个"声音板"（sounding board）——先和数学家充分讨论，帮助他们把模糊的直觉变成清晰的研究问题，然后再开始执行工作。

第三条原则是"产出原生数学产物"。数学家习惯于LaTeX格式的草稿、带有边注的工作文件、有内部引用的论文初稿。系统的输出不是聊天消息，而是一份活生生的"工作论文"，有正文、有边注、有版本历史，和数学家自己手写的草稿一样自然。重要的是，边注会明确标注某个结论的来源，比如"这个剪枝启发式方法来自用户建议；基础上界2.2195来自arxiv上的某篇论文"——这样数学家就能清楚地知道哪些结论是可靠的，哪些还需要进一步审查。

第四条原则是"支持异步交互与灵活引导"。数学研究不是线性的，一个人同时在脑子里跑着好几条思路是常态。这个系统在后台可以同时运行多个并行的"工作流"（workstream），处理不同的子问题，而数学家可以随时介入、调整方向，而不是呆呆等着系统"想完"再给结果。

第五条原则是"通过渐进式披露管理认知负载"。一个长时间运行的研究项目会积累大量信息：高层策略、低层执行日志、多个并行分支的进展、失败的尝试记录。如果全部平铺在一个聊天窗口里，很快就会让人不知所措。系统按照代理层级来组织信息：用户主要与最顶层的"项目协调代理"交互，后者会过滤掉低层代理的执行细节；如果用户想深入了解某个具体工作流的内部过程，也可以随时钻取。

第六条原则是"追踪、管理和传达不确定性"。数学需要极高的严谨性，一个有漏洞的引理可能让整篇论文崩塌。语言模型的输出天然带有不确定性，不能全盘信任。这个系统不是假装不确定性不存在，而是把它当成一个需要被管理的核心变量：通过持续的评审循环、数值验证、系统性引用检查来"消耗计算资源换取可靠性"，并通过高亮和边注来告诉数学家"这部分论证还没有通过充分验证，请你仔细看"。

第七条原则是"保存失败探索的历史"。在数学研究中，知道"什么不行"往往和知道"什么行"同样重要。这个系统把失败的工作流和走到死路的探索，作为头等重要的永久记录保存下来，而不是悄悄重启、抹去痕迹。这些失败记录为后续的新方向提供了宝贵的上下文，体现了数学哲学家拉卡托斯（Lakatos）"反驳是数学进步的基础"这一思想。

四、系统架构：一支无形的研究团队

理解了设计原则，再来看系统是如何运作的，就会觉得一切都很自然。

整个系统的核心比喻是"一支研究团队"。数学家与团队里最高层的"项目协调代理"（project coordinator agent）交谈，就像与一位经验丰富的合作者讨论研究方向。这位协调者不会自己去查文献、写代码或推证明，而是把具体任务分派给下层的"工作流协调代理"（workstream coordinator agents），每个工作流对应一个特定的研究目标。工作流协调者又可以进一步创建更专门的"子代理"来执行具体任务，比如文献检索子代理、编程子代理、Gemini Deep Think证明子代理等。所有这些代理共享一个文件系统，通过内部消息系统沟通，并将各自的工作成果写入共享存储空间。

用一个更直白的类比来说：这就像一家研究所的运作。数学家（所长）告诉项目负责人（项目协调代理）研究方向；项目负责人把工作分配给不同的课题组（工作流协调代理）；每个课题组内部又有具体的分工（子代理），有人查资料，有人写程序，有人推理论。所有课题组的进展汇总到项目负责人那里，项目负责人定期向所长汇报，遇到瓶颈就主动请示。

特别重要的一点是：数学家在整个过程中随时都可以介入。系统不会把数学家"锁在门外"等待结果，而是允许他随时通过聊天界面向项目协调代理发送指令、提供思路、或者调整研究方向。这种双向互动是系统设计的核心——当系统遇到它无法自行解决的困难时，会主动浮现警告，明确告诉数学家"我们卡在这里了，你能帮我们想一个更好的方法吗？"

五、一次真实演练：移动沙发问题的探索

研究团队用一个具体的数学问题来演示系统的工作流程，这个问题来自计算几何领域：在走廊里移动沙发时，能绕过左手边和右手边直角转弯的最大沙发面积是多少？这是一个经典数学问题的变体，研究团队之前已经用AlphaEvolve研究过它的下界，但上界仍然悬而未决。

数学家通过聊天界面上传了相关论文并说明想法："我想研究这篇论文里讨论的移动沙发问题变体的上界证明。"

值得注意的是，项目协调代理没有立刻开始工作，而是先开启了一场对话，充当"声音板"。它回应道："从文章中看，Baek已经证明经典沙发问题中Gerver的下界是精确的。但其他两个变体的上界仍然是开放问题……你想专注于其中一个，还是两个都研究？你是想证明某个特定下界是精确的，还是只要建立任何一个新的严格上界就行？"

经过几轮来回讨论，双方达成一致，明确了研究问题和三个具体目标：文献综述、计算框架构建、执行搜索。数学家正式批准了这个计划，系统才开始分配工作流。

文献综述工作流创建了一个专门的文献检索子代理，利用密集搜索工具找到了关键论文，并通过网络查询工具检索了精确的定理表述和证明细节。计算框架工作流则先让Gemini Deep Think子代理证明高层算法逻辑的合理性，确认它确实能给出严格上界后，再创建编程子代理实现了配套的Python库并附上测试用例。执行搜索工作流在前两个工作流完成后启动，直接调用前一工作流开发的Python库，并通过并行代码执行工具在多台云端机器上同时运行搜索，将结果汇总到工作流报告中。

然而，过程并非一帆风顺。当搜索空间爆炸、初始回溯方法失效时，系统没有悄悄重启，而是触发了一条严格规则：编程子代理的代码在测试通过并被评审代理接受之前，不能标记为完成。评审代理反复拒绝了有问题的代码，工作流被堵塞，项目协调代理因此浮现了一条警告，直接向数学家求助："我们当前的搜索实现效率不足以找到所需结果，文献中也没有太多可以参考的例子。你是否有针对更好剪枝策略的数学直觉？当前方案的详情可以在以下文档中找到。"

数学家阅读了详情，建议了一种基于拓扑的剪枝启发式方法，并指示协调代理创建额外的工作流来同时探索新的上界策略。系统的工作就此重新推进。

最终每个工作流都生成了一份编译好的LaTeX格式报告，包含研究过程的完整说明、带有来源标注的边注、对内部文件的引用，以及经过多轮AI评审确认的内容。这份报告就是数学家可以直接拿来继续深入的工作文件。

六、真实用户：数学家们遇到了什么

系统不只是演示，它已经在少量职业数学家中进行了有限范围的早期测试。研究团队特别强调，以下所有结果都是数学家独立使用系统获得的，没有研究团队的干预或监督。

牛津大学数学家Marc Lackenby用这个系统研究了拓扑学和群论中的若干问题，其中包括《Kourovka笔记本》中编号21.10的开放问题。这个问题问的是：每个有限群是否都存在一种"恰好有限表示"，即某种有限表示使得删掉任意一个关系式后群就变成无穷群？

Lackenby直接把问题打进去，系统同时启动了两个独立工作流，一个尝试证明结论，一个尝试反驳结论。第一个结果是一份被系统自己标记为"有问题"的证明——工作流写出了一个论证，但评审代理发现了漏洞。Lackenby看了这份带漏洞的证明，他的反应很有意思：他觉得这是一个"非常非常聪明的证明策略"，而且当他读了评审代理对漏洞的批注后，他意识到自己知道如何填补这个漏洞。他指出了修补方法，系统随即写出了完整正确的证明。最后Lackenby下载了文件，自行添加了推广和例子，上传后让系统进行最终评审，评审发现了两个小问题，他修正后定稿。Lackenby事后说："AI与数学家之间的来回互动，对于问题的解决至关重要。系统在用户熟悉该领域时效果最好。"他反问道，"让它去解决一个我完全不懂的问题，又有什么意义呢？"

匈牙利数学家Gergely Bérczi则带来了一个关于对称幂表示的Stirling系数的问题，猜想某个二项展开式中的系数不仅严格正，还构成一个对数凹序列。他准备了一份详细的背景说明文档，包括他从AlphaEvolve那里得到的启发（AlphaEvolve曾暗示存在一种可能的归纳公式，但未能解决高指数情况），一并上传作为初始材料。这种他称为"结构化提问"的方式，是他与AI系统合作时总结出的有效方法。系统在两个独立工作流中分别为两个猜想建立了证明（目前仍在人工详细审查中），并为其他未解的猜想提供了详尽的计算证据。值得一提的是，其中一个工作流的子代理在计算枚举后发现原猜想在n=1,2时竟然是假的，但对更大的n似乎成立，并且原来的证明策略也无效。于是系统自动调整了猜想的陈述，并让Gemini Deep Think子代理为修正后的版本提出了新的证明策略。Bérczi也指出合作需要一定技巧："现在要用好它并不是理所当然的事，数学家如何使用这些模型会产生很大差异。"

第三位早期用户Semon Rezchikov则提出了他在研究中遇到的一个技术子问题，关于某类哈密顿微分同胚的特定扰动是否存在。系统与他讨论并厘清了问题的精确定义，然后工作流通过文献检索发现了几个关键技术点，将这些背景知识与问题一起传给Gemini Deep Think，后者产出了包含一个核心引理的证明，且经过仔细检验站得住脚。Rezchikov特别提到了系统在探索失败路径上的价值："我本来可能花一周时间在那个方向上做梦，但现在我直接转向下一个了。"他还评价系统给出的正确证明风格颇为出色："从美学角度来看，它的证明风格是我用过的所有模型中最好的。"

七、基准测试：硬数字说明什么

除了案例研究，研究团队也在客观评测基准上测试了系统的表现。由于这个系统被设计为交互式的长程工作台，研究团队开发了一种专门的"最终答案模式"：绕过初始对话阶段，直接将问题设定为唯一目标，并设置时间上限（内部评测为24小时，FrontierMath评测为48小时），让系统输出一个最终答案。

在一个由职业数学家提供的100道研究级数学问题组成的内部评测集上（所有问题均未被模型训练集污染，答案可以用代码验证），AI数学协作者的得分为87%，而单次调用Gemini 3.1 Pro的得分为57%，单次调用Gemini Deep Think的得分为70%。这意味着系统的代理架构本身（而不仅仅是底层模型的能力）带来了显著的性能提升。

在几个典型的例题分析中，可以清楚看到系统的优势来源。在一道关于几何铺砖的问题中，系统成功地将核心问题转化为布尔可满足性（SAT）问题，并调用Python的PySAT库求解，这种解法明显需要持久文件系统和多轮代码开发能力，而单模型调用很难实现。在一道表示论问题中，系统利用文献搜索工具精确检索了关键定理的条件陈述，避免了单模型调用时因无法查核精确措辞而导致的条件对应错误。在一道兼有理论和计算两面的组合数学问题中，系统将工作清晰地拆分为理论推导工作流和代码开发工作流，理论工作流中评审代理多次发现并纠正了逻辑错误，最终给出了正确答案。

外部评测数据来自Epoch AI组织的FrontierMath第四等级（Tier 4）测试，这一等级由50道题组成，每道题都由教授或博士后级别的数学家设计，被描述为"短期研究项目"，其中一些问题可能在未来数十年内都无法被AI解决。评测采用盲测方式，Epoch AI的工作人员直接操作系统界面输入问题并记录答案，研究团队无法看到问题或观察系统的运行状态。在48道非公开样本题中，系统答对了23道，正确率48%，创下了所有AI系统在该基准上的最高分。与基础模型Gemini 3.1 Pro的19%相比，提升幅度相当可观。系统解出了三道此前没有任何AI系统解出过的题目，同时也有两道题是其他系统解出过而它没能解出的。

研究团队也坦诚地指出了与此前评测结果比较的一个重要差异：FrontierMath评测通常使用Epoch AI开发的标准代理框架，会对模型调用和token使用设置硬性上限；而AI数学协作者使用了自己的工具实现，且没有token数量限制，因此推理成本可能高于此前被评测的系统。

八、挑战与局限：系统也有自己的"死路"

研究团队花了相当大的篇幅讨论他们在开发过程中遇到的真实困难，这种坦诚相当难得。

最令人担忧的问题之一，研究团队称之为"取悦评审者的偏差"，或者更形象地叫"虚假共识"。迭代评审过程是一个动态系统，在理想情况下它会让文件越来越严谨。但当一个代理产出了一个它无法真正修复的有缺陷论证时，整个系统可能会在迭代中收敛到一个"错误已经被包装得足够精巧以至于评审代理也发现不了"的状态。这类论证对人类来说也可能很难识别，正如一些研究者指出的，这是当前AI系统的一个普遍局限。类似的"证明者-验证者动态失效"问题在学术文献中也有记录。

与此相对的另一个极端是"无法终止的争议"，研究团队称之为"非终止"问题。当迭代评审始终无法达成一致时，系统会陷入反复修改与拒绝的死循环。随着自主迭代次数增加，循环往往会退化成越来越多的幻觉推理——这在业内有个形象的名字，叫"死亡螺旋"。研究团队已经实现了若干缓解机制，但根本问题——语言模型之间的意见不一致——目前仍无法彻底解决。早期用户已经学会识别工作流进入这种状态，并相应地降低对其输出的信任。

另一个深层挑战是"系统自主性需要放权"。数学研究本质上是探索性的，事先规划任务序列往往不可能，因为找到正确的步骤顺序本身就等同于解决问题。这意味着系统有时会在无人监督的情况下连续工作数小时，遇到计划外的困难时，当前模型的判断能力远未达到人类的预期水平。如何在允许长时间自主运行与保持用户可控性之间找到平衡，是一个持续的挑战。

还有一个微妙但重要的问题：研究团队早就意识到，数学家倾向于将排版精美的文件与内容的严谨性画等号。大语言模型非常擅长生成完美的LaTeX格式，但这种形式上的完美掩盖了内容上的不确定性。系统试图通过"工作文件"标识和边注来缓解这种误导，但更好的界面设计仍有待开发。团队认为，近期在人机交互领域的AI研究可能提供一些灵感。

九、更大的图景：数学生态系统面临的新挑战

研究团队不仅聚焦于系统本身，还思考了这类工具大规模普及后对整个数学学术生态的影响，这些思考颇为值得关注。

第一个系统性挑战是"保持文献的信噪比"。当AI能够轻松生成格式完美的LaTeX证明草稿，并且能综合大量文献，一旦这类工具被当作自动生成器而非人类引导的协作者，学术界可能会迎来一波"看起来合理但实际上浅薄、渐进甚至有细微错误"的论文洪流。这会增加系统性的"语义噪声"，要求研究者开发新的启发式方法来在更高基准噪声中找到真正的新发现。形式化验证方法和自动形式化技术可能有助于检验正确性，但无法取代人类理解和吸收新发现的含义这一过程。

第二个系统性挑战是"适应同行评审生态"。数学的同行评审依赖深度的人工验证。AI协作的引入制造了一种奇特的不平衡：系统可以在几分钟内生成一篇20页的证明尝试，但一位人类专家可能需要数天才能验证它。如果AI辅助写作变得普遍，而没有相应的可审计追踪机制，这可能给本就依赖志愿者的同行评审系统带来不成比例的负担。研究团队认为，AI数学协作者的边注功能只是提高审计性的一个小小起点，更广泛的社区规范仍有待建立。与此同时，用AI代理替代人类评审有其内在局限：自动评审者擅长局部逻辑检查、代数纰漏发现和缺失引用检测，但目前还缺乏判断一篇论文是否优雅、深刻或真正重要的整体直觉，过度依赖AI评审可能将数学评估简化为机械验证，把引导这个领域的定性人类判断边缘化。

十、评测框架的再思考：衡量什么，才算真正的进步？

研究团队在评测部分提出了一个关于AI数学系统应如何被评价的重要论点，值得单独讨论。

历史上，AI数学进展的衡量依赖于静态问题解答基准，比如MATH、GSM8K，以及最近的IMO ProofBench、FrontierMath、PutnamBench等。这些基准在衡量模型的"原始解题能力"上发挥了重要作用。然而研究团队认为，随着前沿模型在这类基准上已经达到甚至超过专家人类水平，继续单纯提升这一维度的边际价值正在递减，AI辅助数学的进步现在至少部分受限于其他能力——那些反映职业数学家更广泛工作流程的能力。

研究团队指出，一些基准已经在测量与数学研究过程有直接对应关系的能力：DeepSearchQA用于测试通用目的的事实查找能力，Hard2Verify用于测试在竞赛数学证明中发现错误的能力。但据他们所知，目前还没有类似基准专门针对职业研究数学的具体情境。对这些辅助能力的清晰度量（以及对其改进的记录）将越来越重要，有助于减少"参差不齐的AI能力边界"所造成的人类驱动数学与AI驱动数学之间的不匹配。

更重要的是，研究团队认为AI数学系统默认应该被视为"人类在循环中"的系统，进步和成就也应在此框架下衡量。这呼应了他们的根本设计原则：系统存在的首要目的是协助数学家，而不是独立于他们之外取得成功。

说到底，这项研究做的事情，是把一个被忽视了太久的问题摆上了台面：AI在数学领域的真正价值，不只是解出更多竞赛题，而是能否真正融入数学研究的日常——那些混乱的、迭代的、充满失败的日常。

谷歌DeepMind这套系统给出的答案，是一个有状态记忆、有并行工作流、有严格评审机制、会主动求助、保存失败历史的工作台。三位早期用户的经历——Kourovka笔记本里的问题被解决、Stirling系数猜想有了新进展、哈密顿微分同胚的引理被优雅证明——说明在合适的设计下，人与AI之间的互动可以产生双方单独都无法达到的结果。

系统也有明显的局限：虚假共识、死亡螺旋、自主性与可控性之间的张力。研究团队的坦诚令人印象深刻，他们没有假装这些问题不存在。

48%的FrontierMath Tier 4成绩是当前已知的最高分，但研究团队自己也指出，这个数字背后有更高的计算成本，直接比较需要谨慎。更重要的提醒在于：解题基准只能测量研究的一个截面，而协作效能、探索性思维、不确定性管理这些维度，目前还没有成熟的评测框架。建立这样的框架，也许才是AI辅助数学领域下一个真正重要的任务。

对这项研究感兴趣的读者，可以通过arXiv编号2605.06651查阅原论文的完整内容，一窥这套系统更多的技术细节和案例数据。

**Q&A**

Q1：AI数学协作者系统是否可以公开使用？

A：目前AI数学协作者处于有限范围的早期测试阶段，只有少数受邀的职业数学家可以使用。谷歌DeepMind表示，目标是在未来开发出能够提供更广泛访问权限的产品，但目前尚未向公众开放。感兴趣的读者可以关注谷歌DeepMind的官方动态。

Q2：AI数学协作者和直接使用Gemini聊天有什么本质区别？

A：两者的根本区别在于"状态性"和"工作流架构"。直接使用聊天模型，每次对话结束就没有记忆，无法保存研究历史，也不能并行处理多个子问题。AI数学协作者有持久的共享文件系统，能同时运行多个工作流，保存失败探索的记录，并通过严格的评审循环验证结论，是一个完整的研究工作台，而非单次问答工具。

Q3：AI数学协作者的评审代理真的能发现数学证明中的逻辑错误吗？

A：系统的评审代理能够发现很多逻辑错误，Kourovka问题案例中评审代理发现的漏洞，甚至启发了人类数学家找到修补方法。但系统也存在"虚假共识"的风险：当代理无法真正修复某个错误时，可能最终生成一个包装得足够好以至于评审也通过的有缺陷论证。研究团队建议数学家对系统输出保持批判性审查，不能完全依赖自动评审的结论。