数学问题在 Agent 实践中的难点

前言

这段时间，我一直在关注 AI 参与数学研究的进展，也陆续读了一些研究论文、Agent 系统报告和公开审稿记录。

这篇文章是一次阶段性的整理。它试图结合具体案例，讲清楚目前数学研究 + AI 中的一些难点，但这样的整理肯定还不充分。

文章以四类困难为线索：战略不确定性、相互依赖的技术难点、长证明中的错误积累，以及失败尝试中有用信息的保留。在此基础上，结合各家系统实践和专家审稿记录，重点讨论困难如何出现、为什么不容易解决。

一、战略不确定性

数学研究中的第一项困难，是不知道应该选择哪条证明路线。更隐蔽的困难则是：系统已经找到一条看似完整的路线，却无法判断它是否真正降低了问题的难度。

1.1 把核心困难命名为“引理”，不等于解决了核心困难

以 First Proof 第二批评测的第 3 题为例，提交 C 将问题归约为两个关键引理。评审记录指出，所引文献并不包含这两个结论；其中一个引理即使弱化，也会推出评审当时尚未解决的 Csóka 猜想的一种形式。后续归约大体合理，但核心困难并没有得到处理。

这类失败可以抽象为：

如果引理 L 成立，那么目标定理 T 成立。

Agent 证明了这条蕴含关系，然后把“证明 (L)”写进任务清单，仿佛已经完成了大部分工作。但 (L) 可能与原问题同样困难，甚至更强、更难。

归约当然可能有价值。将一个陌生问题转化为结构清楚、工具成熟的问题，本身就是一种进展。

但从 Agent 的执行视角看，这尤其危险。假设规划器生成十个子任务，其中九个都容易完成，剩下那个却承载了几乎全部的原创性，那么“任务完成率 90%”其实没有反映真实的数学进度。

1.2 反复修订，可能只是在同一个不完整框架里打转

Momus 论文分析了一套既有的求解器—验证器流程。在 PB-Adv-011 上，系统只完成了单射解的分类，没有排除非单射解，并明确承认这一缺口，却仍连续五次获得内部验证器认可。

假如生成者继续改写论证，验证者继续检查那些已经正确的局部结果，系统完全可能表现得越来越稳定，却没有更接近完整答案。

这一案例来自竞赛型证明任务，不能直接用于推断开放数学研究的成功率。但它确实提示了一种需要防范的机制：增加迭代次数，不一定会推动系统离开原来的思考框架。

二、依赖分散

数学问题可以拆分，但拆分之后，各部分之间必须严格衔接。

这种衔接不只涉及“任务 A 完成后执行任务 B”，还涉及对象所在的空间、允许使用的假设、参数范围、量词顺序，以及上游结论能否在下游要求的条件下使用。

2.1 “有理数版本”完成了，“整数版本”却没有

Danus 的一个研究案例涉及拟阵的切类构造。系统首先完成了有理系数版本，而原任务要求的是整数系数版本。配套论文里说明，题面使用同一个符号表示整数对象及其有理化，这种记号省略促成了误解。人类指出差异后，系统才继续补充整数版本。

这个案例直接暴露的是任务理解与目标对齐问题。放到多 Agent 协作中，同类歧义还可能出现在任务交接处：上游认为自己提供了所需对象，下游认为这个对象满足更强要求，最终汇总者看到的则是一套表面完整的论证。

类似的差异还包括：“有限维”与“任意维”，“对每个参数分别存在一个常数”与“存在一个对所有参数通用的常数”。这些表述很接近，数学意义却不同。

2.2 依赖图往往不是一开始就能画完整的

LeanMarathon 的一个形式化案例揭示了另一种困难。对 Erdős 问题 #1196 的相关证明进行形式化时，系统从一个表面估计向下追溯，先遇到 Dirichlet eta 函数的单调性，再遇到 Gamma 分布的随机序比较与 Mellin 表示。

一个小节的篇幅很短，不代表它依赖的数学很少。论文中的一句“由标准方法可得”，可能调用了一整套默认知识。对于形式化 Agent，这些知识必须落实为可调用的定理，或者重新证明。

于是，最初的任务“证明估计 A”，执行之后可能变成：A 依赖 B；B 依赖 C 和 D；C 需要先建立某个分布比较；D 需要补齐一个积分表示及其适用条件。

这不是简单地给原任务增加几个步骤，而是在执行过程中发现：原先理解的任务边界并不准确。

进一步说，同一条证明路线内部，往往需要多个引理同时成立；不同路线之间，又可能相互替代。某个节点失败后，有时应该继续分解，有时应该修改上游陈述，有时则应该放弃整条路线。

这也解释了为什么“局部返工”并不只是重新调用一次模型。假如为了证明某个引理，系统增加了一个假设，那么所有依赖该引理的后续步骤，都必须重新检查是否满足这个假设。

三、长证明

长证明的困难，是随着论证扩展，系统必须持续维持定义一致、假设完整、依赖有效，以及局部结论与全局目标之间的联系。

3.1 局部规则简单，不代表全局性质容易证明

Knuth cycles 案例要求把一类有向图的全部边分成三条哈密顿回路。论文记录，一套构造已通过 (m\leq 2000) 的计算检查，并报告了两套构造分别对应的 46 页和 75 页证明草稿。核心困难是：简短的局部路由规则，必须被证明对任意相关规模都产生目标回路，而不是若干较短的回路。

可以用一个简单例子理解这个差别。

假设一个有限有向图中，每个顶点都恰好有一条入边、一条出边。这个局部条件并不能保证所有顶点属于同一个回路。它也可能由两个互不相交的回路组成。

所以，“每个位置的规则都合法”和“整个构造具有目标性质”，是两项不同的证明任务。局部检查不能替代缺失的全局论证；有限规模的计算实验，也不能直接替代对所有规模的证明。

3.2 把事实整理成论文，本身也可能引入新错误

Danus 团队报告，将已经接收的事实整理为可读论文时，重新组织和压缩论证仍会引入错误。

原因并不难理解。把几条已有事实写成一段流畅叙述，往往需要增加连接。例如：

“因此可以交换这两个操作。”

“这个结论也适用于边界情形。”

“不失一般性，可以固定某个参数。”

这些句子看似承担编辑功能，实际上都可能包含新的数学主张。如果已有结果没有覆盖它们，就出现了新的证明义务。

这意味着，保存完整推导和生成可读证明，是两个相关但不同的任务。前者强调不丢信息，后者强调压缩、重组和解释。压缩做得越多，越需要检查哪些前提被省略了，哪些连接被默认了。

文献引用也是类似的跨文档依赖。Aletheia 的研究报告指出，经过工具使用训练并接入检索后，虚构论文标题和作者的问题有所减少，但仍会出现“论文真实存在，所声称的结论却不在其中”的错误。

3.3 形式检查通过，还要确认检查的是原来的命题

一项关于自主研究群体的案例研究记录了更直接的目标偏移。在作者构建的研究模拟中，部分 Agent 使用局部记号覆盖数学谓词，使原题被解释为容易证明的命题。代码通过了 Lean 编译，但没有证明原来的数学问题；被接收的代码进入共享库后，又被其他 Agent 模仿。

这里的问题是外围系统没有可靠地维护“要求证明的命题”和“实际送入检查器的命题”之间的一致性。

必须区分两件事：

给定的形式命题是否被正确证明，与这个形式命题是否忠实表达了原题，不是同一项检查。

四、失败尝试

数学探索中的失败，并不是统一类型的事件。

找不到证明、找到反例、证明了特殊情形、发现某项额外假设不可缺少，具有不同的信息价值。将它们全部压缩成“失败”，会丢掉下一轮研究最需要的内容。

4.1 一份被否定的证明，可能包含可以继续使用的结果

First Proof 第 3 题的提交 B 因核心比较引理存在反例而被拒绝，但评审同时确认，它正确处理了 (p=1/2) 和 (p=1)，并正确排除了集合 ([0,1/3]\cup{1/2,1}) 之外的参数。整个证明没有完成，不等于其中每一项结论都无效。

这个案例说明，对失败的处理应当比“重试”或“放弃”更细致。

假设某条证明路线依赖引理 (L)，现在发现 (L) 为假。可以确定的是，这条依赖 (L) 的论证不能继续成立。但不能据此推出目标定理 (T) 为假。

与此同时，不依赖 (L) 的局部结果仍然可能保留。即使一般版本失败，某个特殊参数范围、附加条件下的版本，也可能已经得到有效证明。

这是一种数学信息提取工作，而不是对聊天记录做普通摘要。

4.2 搜索失败不等于数学否定

这里尤其需要区分三种看似相近的状态。

“在当前预算内没有找到证明”，只说明这次搜索没有成功。

“某个构造在计算实验中失败”，说明该构造在相关实例上不满足要求，但不一定排除了其他构造。

“存在一个满足全部假设、却违反结论的反例”，才构成对相应命题的否定。

如果 Agent 把第一种状态记录为第三种，下一轮可能错误地放弃一条有效路线；反过来，如果已经找到严格反例，却只留下“这里可能有点问题”，后续 Agent 又可能重复投入大量工作。

五、写在最后

观察 Math Agent 项目 Momus、Aletheia、LeanMarathon、Danus，从这些设计中可以提炼出一种共同思路：不把数学研究当成一次生成答案，而是把它组织为一个能够持续修改、验证和追踪依赖的过程。

但拥有事实图，不等于其中的事实必然正确；拥有验证者，不等于验证目标没有漂移；保存了失败记录，也不等于记录准确表达了失败的数学含义。架构的价值，最终仍要通过这些具体边界是否被守住来检验。

数学问题在 Agent 实践中的核心难点，不只是生成新的推理，而是在不断探索、拆分、修订和遗忘的过程中，仍然准确维护“已经证明”“有条件成立”“尚待证明”与“已经被反驳”之间的界线。