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

DeepMind 构建数学家多 Agent 协作工作台，支撑开放式研究的异步状态化探索。

前置知识

LLM Agent（智能体）

由大语言模型驱动的自主执行单元，能调用工具、维护状态、按规划完成多步任务。它把单次 prompt 升级为带记忆、可反馈、可分支的工作流，是当前最强的数学 AI 系统所采用的范式。

本文系统本身就是 LLM Agent 的层级协作，理解 Agent 与单次调用的区别是看懂架构的前提。

多智能体协作（Multi-agent system）

多个具有专门职责的 Agent 通过消息系统协作完成任务，通常采用层级或去中心化结构。每个 Agent 只负责自己擅长的工作流片段，整体复杂度通过分工与编排被摊薄。

本文核心架构就是 project coordinator → workstream coordinator → 专门子 Agent 的三层组织，没有该概念无法理解系统如何分摊开放式研究任务。

FrontierMath 基准

由 Epoch AI 发布的研究级数学基准，包含 Tier 1-4 四档，Tier 4 是 50 道由专家构造的短期研究项目级问题，被业内公认为当前最难的 AI 数学基准。

本文系统在 FrontierMath Tier 4 取得 48% 准确率创历史新高，是论文最核心的定量成果。

形式化证明与验证

通过 Lean、Coq 等交互式证明助手，把每一步推理写成机器可校验的形式化证明。AlphaProof 即此类系统，正确性由证明助手给出，与靠 LLM 自审的非形式化路线有本质差异。

文中多处把 AlphaProof、Aletheia 列为未来集成方向，理解形式/非形式证明区别才能体会当前系统可信度的边界。

研究动机

现有 AI-for-math 系统虽然在不同维度取得突破，但都难以真正支撑数学家的日常工作流。自主推理系统如 Aletheia 偏向端到端解题；进化搜索如 AlphaEvolve 只能跑特定优化；形式化证明器如 AlphaProof 强于机械化验证但门槛高；商业聊天界面虽然易用，本质上却是无状态、瞬时的单次调用。真实数学研究是跨数日甚至数周的高度迭代过程：管理不确定性、合成零散文献、撰写与修订中间成品、追踪多分支假设树，数学家不得不充当各个独立 AI 工具之间的'人工连接组织'。这种断层意味着当前 AI 能力虽强，但落地到数学家工作流时仍碎片化严重，缺乏一个真正为探索性研究而生的协作环境。

本文的目标是本文的目标是构建一个名为 AI co-mathematician 的交互式工作台，把已有的 AI 推理能力（Gemini 3.1 Pro、Deep Think）按数学家真实的研究范式编排起来，提供一个有状态、异步、可被用户随时介入的协作空间，让 AI 成为数学家在开放式研究中的真正协作者而非孤立答题器。系统目标覆盖从文献检索、头脑风暴、计算探索、猜想形成到非形式化证明的完整链路，并允许嵌入 AlphaProof、Aletheia、AlphaEvolve 等专业引擎。

与已有工作不同的是，本文的独特切入角度是借鉴软件工程领域近年 AI 编码环境（Antigravity、Claude Code、Codex）的成功经验——版本控制、持续测试、设计文档——指出数学界至今没有对应的 'agentic flow'。文章把不确定性管理、分支失败历史保留、渐进信息呈现等软件工程成功范式移植到数学研究中，从而打开此前被忽视的'编排'这一新维度。区别于 AlphaProof 等单点突破，本文强调'harness'而非'模型'的贡献，主张把现有模型能力通过编排放大数倍而非再训一个新模型。

核心方法

系统整体上是一个运行在共享文件系统上的多 Agent 层级架构，最顶层是 project coordinator，直接与用户对话、把任务分发给若干 workstream coordinator，每个 workstream 又可以派生专门子 Agent（编程子 Agent、Gemini Deep Think 子 Agent、文献检索子 Agent 等）。所有 Agent 异步运行，用户任何时刻都可以介入而不被阻塞。系统基于 Gemini 3.1 Pro，没有依赖任何定制模型行为或训练——它是一个'为商用模型服务的 harness'。这与软件工程中 Claude Code、Antigravity 的范式一致：模型能力相同，价值来自编排。

核心创新是把'不确定性'作为一等公民来编排，而非掩盖它。具体机制有三：(1) 硬性程序化约束——代码必须通过测试和审稿 Agent 才能被认作完成，报告必须通过多轮审稿才能发布，避免 Agent 取巧走捷径；(2) 保留失败探索作为持久记录——dead end 不是被悄悄丢弃，而是显式存盘供后续 Agent 与用户参考；(3) 'Working paper'作为活文档——所有结果以带边注的 LaTeX 文档形式呈现，边注追溯每条断言的来源、可信度、争议性，把 AI 的隐式过程显式化。这三点区别于任何单一功能型 AI 数学系统。

方法步骤详情

方法分为六个步骤：(1) 引导对话阶段——project coordinator 不立即开始解题，而是与用户反复确认问题边界、研究目标，避免 zero-shot 的 prompt 不全问题；(2) 目标形式化——把对话沉淀为结构化研究问题与若干 Goal，用户显式批准后才进入下一阶段；(3) 研究分支——为每个 Goal 派生独立 workstream，多个 workstream 并行；(4) 子 Agent 调度——workstream 内部根据需要调用编程 Agent、Gemini Deep Think、文献检索 Agent 等；(5) 交互式 steering——workstream 遇到瓶颈时主动向用户求助，用户可随时插入新方向或修改策略；(6) 产出与审稿——workstream 产出经多轮审稿 Agent 反复评审的 LaTeX 报告，包含边注、内部链接、外部引用，再交由 project coordinator 汇总。

技术新颖性

技术新颖性不在于新的基础模型或新算法，而在于工作流编排模式本身。文章贡献了七个明确的设计原则（拥抱超越证明的数学、支持意图迭代、产出原生数学制品、异步交互、渐进信息披露、追踪不确定性、保留失败历史），并把它们工程化为可复用的 Agent 层级、文件系统消息协议、审稿循环机制。把'证明以外的数学活动'和'失败探索的价值'这两个常被忽视的维度显式纳入系统设计，是本文相对 AlphaProof、Aletheia、AlphaEvolve 的本质差异。

**Figure 1**: A simplified diagram of the organization of agents in a typical AI co-mathematician workspace.

**Figure 2**: In the initial exploration phase, a conversation between the user and the project coordinator results in an approved research question and project goals.

**Figure 3**: Once the research question and goals are defined, the project coordinator schedules workstreams to make progress towards the goals.

**Figure 4**: A single workstream consists of a sequence of actions taken by a workstream coordinator agent.

实验结果

核心定量成果分两块。内部基准（$N = 100$ 道研究级、有代码可验答案的问题）上，AI co-mathematician 显著超过 Gemini 3.1 Pro 与 Gemini Deep Think（图 5）。例：几何铺砖题中它把核心问题规约为 SAT 用 PySAT 求解，两个基线走纯理论路线均失败；表示论题中它靠文献检索拿到精确定理陈述后正确应用，基线因不能查文献而错配假设。外部 FrontierMath Tier 4 上系统取得 $48\%$（$23/48$ 道，去掉 2 道公开样本）准确率，刷新所有已评估系统最高分，相较其底层基线 Gemini 3.1 Pro 的 $19\%$ 提升约 $2.5\times$；其中 3 道题首次被 AI 解出，但也有 2 道此前可解的题被错过。定性层面三个案例有说服力：Lackenby 借系统解决 Kourovka Notebook 开放问题 21.10（每个有限群是否都有 just-finite 表达）；Bérczi 用系统证明 Stirling 系数相关两条猜想；Rezchikov 用系统得到一个 Hamiltonian 系统引理。

**Figure 5**: Accuracy scores for Gemini 3.1 Pro, Gemini Deep Think, and the AI co-mathematician on an internal research mathematics benchmark.

查看结构化数据

任务	指标	本文	基线	提升
FrontierMath Tier 4	问题解决准确率	48% (23/48)	Gemini 3.1 Pro 19%	+29 个百分点（约 2.5×），刷新该基准历史最高分
内部研究级数学基准（100 题，代码可验证）	准确率	显著优于两个基线（具体数值见图 5）	Gemini 3.1 Pro 与 Gemini Deep Think	在几何铺砖、表示论、组合等题目上展现质变差距

局限与改进

作者在第 7 节坦承若干局限。Reviewer-pleasing bias（虚假共识）—— 当 Agent 修复不了缺陷论证时，可能为通过审稿而收敛到'看似合理但仍有错'的版本，错误甚至人类都难发现，与 prover-verifier 动力学已知病理一致。Intractable disagreements（不可终止）—— 审稿循环陷入反复否决时会出现 'death spiral'，后续迭代越来越幻觉化，作者至今只能靠启发式缓解，缺乏 $\text{iter} \le k$ 硬性上限。System autonomy requires ceding control —— 系统允许数小时无人工介入的自主运行，但当前模型在遇到未规划困难时判断力远不如人。Semantic meaning of representations —— 数学家看到精美 LaTeX 会潜意识假定其内容严谨，但 LLM 排版能力远强于逻辑验证能力。系统性风险方面，自动化生产出'看似严谨但肤浅/微瑕'的论文会污染数学文献信噪比。

独立分析的弱点

独立分析下系统还有几个明显弱点。第一，审稿循环的非终止性没有形式化保障，只靠启发式缓解，应当引入严格的迭代次数上限 + 升级到 project coordinator 的硬性协议；第二，系统当前对所有失败探索都保留，但缺乏对其后续利用率的统计与压缩，长期运行的项目 workspace 会膨胀；第三，用户每次介入都需要主动查看 chat 才能发现系统求助，缺乏更主动的实时通知（桌面通知、关键事件 trigger）；第四，FrontierMath Tier 4 评估中 2 道此前可解的题被错过，提示系统在某些题型分布上反而不如单一强力推理模型，可能因为工作流开销压垮短小问题；第五，目前所有审稿都是非形式化的，最终可信度仍受限于 LLM 自身校验能力，没有与 Lean/Coq 的形式化回环；第六，缺少数值化的人机交互评估指标——用户节约时间、用户认知负担等都未量化。

未来方向

作者明确指出的方向包括：把 AlphaProof、Aletheia 等形式化或强推理引擎作为子 Agent 集成进来，让非形式化结果可以与形式化校验打通；用 AlphaEvolve 这类进化搜索替换当前的简单并行代码执行，提升搜索密集型子任务能力；构建面向专业数学研究的交互式评测基准（区别于静态解题基准），DeepSearchQA、Hard2Verify 被列为可行起点。基于成果可延伸的方向还包括：把'失败探索的负空间'反向用于训练数据增强（把系统实际遇到的死胡同构造为难例）、跨项目共享已验证引理的小型数学知识库、与论文写作工具（arXiv 提交、Overleaf）直连。

复现评估

复现难度较高。文章没有公开代码、prompt、Agent 拓扑或审稿 prompt；系统目前只通过受限内部发布（limited initial release）开放给少数专业数学家使用，远未公开发布 API。FrontierMath Tier 4 的评测是 Epoch AI 盲测进行，作者团队并未看到具体题目，外部研究者无法复现该评测。基线 Gemini 3.1 Pro 的 19% 数据来自 Epoch AI 历史测试但具体条件不明。内部 100 题基准不公开。算力方面，作者说每个 attempt 大致相当于一次长 AI 辅助软件工程会话的调用量，但未给具体 token 数、GPU 小时或美元成本。论文还自定义了工具实现（不基于 Epoch 标准 harness），并设 24 小时（内部）或 48 小时（FrontierMath）的硬性时间上限，这些都增加了精确复现的门槛。

AI 协数学家：用智能体式 AI 加速数学研究 AI Co-Mathematician: Accelerating Mathematicians with Agentic AI