AI Co-Mathematician：数学家不需要AI替他思考，他需要AI替他记得自己走到了哪

AI Co-Mathematician：数学家不需要AI替他思考，他需要AI替他记得自己走到了哪 --- ## 证明之外的数学 数学论文读起来像一座冰山——你看到的只有水面之上那10%的精炼证明，水面之下是90%的试错、死胡同、被推翻的直觉、和凌晨三点突然醒来的灵感。 Thurston说过，数学从根本上说是一项社会事业，目标是推进人类理解，而不是制造形式证明。Putnam更直接：把数学还原成孤立的逻辑形式主义，忽略了这门学科深刻的准经验现实。 但今天的AI-for-math系统，几乎都在盯着那10%。AlphaProof在做形式验证。Aletheia在做自主推理。AlphaEvolve在做进化搜索。它们都很强，但它们是**引擎**，不是**工作流**。 一个数学家的日常工作不是"证明一个定理"，而是管理一个项目：修改问题表述、查文献、跑计算、被反例打脸、重新调整方向、和别人讨论、写下阶段性笔记、再被打脸、再调整。这个过程可能持续数周、数月。而当前的工具——ChatGPT式的对话界面、专门化的证明器、孤立的计算脚本——要求数学家充当所有这些碎片之间的"人工连接组织"。 Google DeepMind的团队看到了这个裂缝。他们问的不是"AI能不能自己证明定理"，而是： **"AI能不能成为一个真正的合作者——有状态、有记忆、能并行工作、会承认自己不确定、并且记得所有死胡同？"** 这就是AI Co-Mathematician。 --- ## 七个设计原则：把混乱当作第一性原理 这篇论文的框架不是技术架构图，而是七条设计原则。每条原则都在对抗一种"AI应该整洁"的幻觉。 ### 原则1：拥抱超越证明的数学 真正的数学发现是混合的：精炼研究问题、翻遍文献、头脑风暴、跑数值模拟来建立直觉。系统必须支持这种全谱系活动，而不是只索引最终定理。 ### 原则2：支持意图的迭代细化 数学家常常不知道自己到底想问什么。Cantor说："在数学中，提出问题的艺术比解决问题更有价值。"系统必须允许用户从模糊的想法开始，通过对话逐步聚焦——而不是要求用户一上来就写出完美的问题描述。 ### 原则3：产出原生数学工件 不是聊天记录，不是半成品手稿，而是一个活的"工作论文"——带有内联注释和页边注，标明每个声明的来源、每个引理的不确定性级别。让数学家能重建mental model，知道哪部分铁打不动、哪部分还在晃。 ### 原则4：异步交互与灵活引导 数学研究不是线性的。系统不是单个对话机器人，而是一个异步团队。多个专业agent并行工作，用户随时可以和项目协调器agent对话来干预、绕过当前约束、重新引导研究方向。如果agent卡住了，它**透明地**标记障碍并请求人类协助——而不是默默重启或给出胡说八道的答案。 ### 原则5：通过渐进披露管理认知负荷 当多条探索路径并行、从死胡同回溯、重用中间结果时，一个长长的非结构化聊天会迅速变得不可用。系统采用渐进披露：默认只向用户展示项目协调器agent过滤后的高层策略，但用户随时可以深入到任何并行agent的底层执行细节。 ### 原则6：跟踪、管理和传达不确定性 数学要求严谨。一个错误的引理或虚构的引用可以毁掉整篇论文。基模型推理的不可预测性给这个精确领域引入了不确定性。系统不是隐藏这种摩擦，而是围绕不确定性的生命周期来设计架构： - **跟踪**：详细的版本历史，监控声明如何演变或被质疑 - **管理**：用计算换验证——持续审查、数值模拟、系统性引用检查 - **传达**：当审查过程在某个论证段落卡住时，用高亮和页边注标记给用户 不确定性不是错误状态，是需要编排的核心变量。 ### 原则7：保留失败探索的历史 在数学研究中，知道什么**不**管用往往和知道什么管用一样重要。系统不把死胡同当作垃圾扔掉，而是把它们作为一等公民永久保存。失败的目标、耗尽的策略、被推翻的假设——所有这些"负空间"构成了后续探索的上下文。因为真正的数学进步很多时候是从refutation中诞生的。 --- ## 实践中的架构：层级agent + 共享工作空间 AI Co-Mathematician的架构不是平面的，而是层级化的，模仿人类研究团队的组织方式： ``` 用户 ↕ 项目协调器 agent（Project Coordinator） ↕ 工作流协调器 agent（Workstream Coordinator）× N ↕ 专业子 agent（Specialized Sub-agents） ``` 所有agent共享一个文件系统和内部消息系统。项目协调器负责和用户对话、理解意图、定义研究问题和高层次目标。目标确认后，协调器将它们分解成并行工作流，每个工作流由一个工作流协调器管理。 ### 实际案例：移动沙发问题 论文用一个具体场景演示系统的工作方式。用户想探索计算几何中的一个开放问题：证明"能绕过左右两种直角弯道的沙发"的最大面积上界。 **初始探索阶段**：项目协调器不是立刻开始解题，而是先和用户对话，充当"共鸣板"： > "从文献看，Baek已经证明了Gerver下界在经典沙发问题中是紧的。但另外两种变体的上界仍然是开放的……你想专注于其中一个，还是两个都做？你的目标是证明某个特定下界是紧的，还是只是建立任何新的严格上界？" 用户澄清后，协调器提出正式的研究问题和目标，用户修改措辞并确认。这个对话确保下游资源被导向数学家**真正**想问的问题。 **分支研究阶段**：三个并行工作流同时启动： 1. **文献综述**：专门agent搜索沙发问题上界的关键论文，直接查询重要引用，提取关键引理的确切陈述和证明。 2. **计算框架**：工作流协调器先让Gemini Deep Think证明某种计算框架能给出严格上界，然后创建coding agent实现Python库，附带测试和演示案例。 3. **执行搜索**：在计算框架完成后，启动分支定界搜索，使用并行代码执行工具在云端机器上扩展搜索。结果汇总到工作流报告中。 所有证明在当前原型中都是非正式的，但架构预留了接入AlphaProof（形式证明）或Aletheia（更强的非正式推理）的接口点。 --- ## 基准测试：FrontierMath Tier 4 的48% 除了定性案例，论文还报告了定量结果。AI Co-Mathematician在FrontierMath Tier 4上达到了**48%**——这是所有AI系统的新高。 但作者很谨慎：这个数字不是重点。重点是"一个为交互式、开放式研究设计的系统，同时也能在静态基准上表现优异"。如果反过来——只为刷榜优化——得到的系统很可能不适合真正的研究流程。 这种"能力基准 + 工作流程验证"的双重评估策略，本身就反映了论文的核心理念：数学AI不能只比解题分数，要比谁能融入真正的研究生态。 --- ## 局限：它还不是完美的同事 作者坦诚地列出了系统的边界： 1. **当前子agent基于标准LLM调用**，尚未接入AlphaEvolve、AlphaProof或Aletheia等高级引擎。架构上留了接口，但集成还在未来。 2. **所有证明都是非正式的**。形式验证的缺失意味着agent可能在"看起来对"和"真的对"之间有灰色地带。 3. **人类介入的频率不确定**。系统在什么时候该自己探索、什么时候该停下来问人，这个阈值没有系统性的优化，目前依赖启发式规则。 4. **失败历史的利用还不自动化**。死胡同被记录了，但agent还没有自动从失败历史中归纳模式、生成新假设的能力。 5. **仅限于数学**。虽然设计原则可能适用于其他研究领域，但当前实现是针对数学工作流优化的。 --- ## 核心论点回顾 AI Co-Mathematician不解决"AI能不能自动证明定理"这个问题。它解决的是另一个更基础的问题：当AI真的能证明定理时，数学家怎么和它一起工作？ 当前的工具生态像一堆独立的强力引擎——证明器、搜索器、对话模型——数学家被迫充当它们之间的粘合剂。AI Co-Mathematician提供了一个编排层：一个有状态的、异步的、层级化的agent系统，模仿人类研究团队的工作方式。 它的核心创新不在任何一个单一技术，而在**七条设计原则的整体性**：支持意图迭代、产出原生工件、异步并行、渐进披露、不确定性生命周期管理、以及最重要的——**把失败当作一等公民保存下来**。 这个视角的转变是深刻的：从"AI帮我解题"到"AI和我一起探索"。前者把AI当计算器用，后者把AI当同事用。而真正的数学研究，从来都不是解题，是探索。 --- ## 论文信息核对 | 项目 | 内容 | |------|------| | 论文标题 | AI Co-Mathematician: Accelerating Mathematicians with Agentic 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 | | arXiv ID | arXiv:2605.06651v1 [cs.AI] | | 提交日期 | 2026年5月7日 | | 核心方法 | AI Co-Mathematician：有状态交互式数学研究工作台，层级agent架构 | | 关键技术 | 项目协调器agent、工作流协调器agent、并行工作流、渐进披露、不确定性生命周期管理、失败历史保留 | | 设计原则 | 7条：超越证明、意图迭代细化、原生数学工件、异步交互、渐进披露、不确定性管理、保留失败历史 | | 实际案例 | 移动沙发问题（计算几何开放问题）——文献综述+计算框架+分支定界搜索 | | 基准结果 | FrontierMath Tier 4: 48%（所有AI系统新高） | | 架构预留 | AlphaProof（形式证明）、Aletheia（自主推理）、AlphaEvolve（进化搜索）接口 | | 代码/产品 | 有限初始发布，目标未来更广泛开放 | | 智柴状态 | 未讨论（2026-05-09确认） | --- > 读完这篇论文我在想一件事。费曼有个习惯：他会在黑板上写满公式，然后全部擦掉，只留下最核心的那条。但他始终记得那些中间步骤——因为它们定义了他为什么相信最终结论。AI Co-Mathematician做的本质上就是这件事：它帮数学家记住那些"被擦掉的中间步骤"，包括所有的错误尝试。因为在一个真正困难的问题面前，你知道哪条路不通，往往和你知道哪条路通一样珍贵。