Euler:以人為中心的多智能體數學發現系統

数学研究是科学发现的重要动力。近来 AI for mathematics 的进展表明，语言模型智能体已经能求解有难度的问题，甚至写出相当长的数学证明。但现有工作大多围绕「拿到最终答案」展开，这种取向带来两个麻烦。第一，结果背后的探索过程很难被研究者看懂。人们只看到结论，看不到路径上做过哪些取舍、放弃过哪些思路。第二，长时间运行的研究会遇到上下文碎片化。一个没有依据的断言一旦进入推理链，就可能在后续步骤中被反复引用，层层放大，最后很难追查源头。Euler 这篇论文针对的正是这两个问题。

作者提出了一个以人为中心的数学研究系统，核心贡献是一套共享的、结构化的研究过程表示。系统不再只保存答案，而是把研究过程本身当作可以被追踪、被复用、被检验的对象。论文通过三个数学研究案例展示系统能力，并说明了已实现的系统及其软件验证。Euler 的技术核心是研究图（research graph）。图中的节点与连接把数学陈述、前提假设、证明依赖关系、备选思路、失败的尝试以及验证证据组织在一起。这里有一个值得注意的设计：失败的尝试和备选方案也被当作一等公民记录下来，而不是在最终文稿里被抹掉。这样，研究者能顺着图回看一个结论是怎样一步步长出来的，也能看清它依赖哪些前提。对智能体来说，这张图是持久化的、与任务相关的知识来源。

多个 agent 在规划、协作和验证时，可以只取出当前任务需要的那部分图，而不必把整段历史塞进上下文，所以跨会话也不会丢失线索。依赖关系和验证证据直接挂在节点上，使「某个断言有没有依据」变成一个可以查询的问题，这有助于阻止无依据的说法在推理步骤之间传播。系统的另一项能力是交互：研究者可以选中图上的某个节点，该节点关联着一个已保存的团队状态（team state）。借助它，研究者能回到智能体当时的推理现场，再通过继续交互去探索别的方向，而不是从头再跑一遍。在实验与评估方面，先要说清一点：摘要给出的信息偏向系统描述，没有列出基准测试上的具体指标，所以这里不对任何数字做推断。论文采用的是案例研究的方式，选取三个数学研究案例，演示 Euler 在真实研究场景里如何工作。这些演示涉及几个层面：研究图如何随探索逐步生长，失败尝试和备选路径如何被保留下来，验证证据如何挂到对应的陈述上，以及研究者如何选中节点、恢复团队状态并换一个方向继续。除案例之外，论文还描述了已经实现的系统和它的软件验证，也就是确认系统各部分按设计运行。

这类评估回答的问题是「系统能否支撑一个完整的研究流程」，而不是「在某个榜单上得分多少」。读者应当把它看作一篇系统与交互设计方向的论文，证据主要来自案例演示和工程层面的验证，而不是大规模的定量对比。这也留下了后续工作的空间：图结构对抑制无依据断言传播、对长程研究的实际帮助，仍需要更系统的对照实验来量化。从行业意义看，Euler 把 AI 数学的重心从「答案对不对」移到「过程能不能被理解和复用」。对数学家来说，这更接近真实的研究方式：一个定理的价值不只在结论，也在证明的结构、试过的死路和各步骤之间的依赖。把这些显式保存下来，AI 才有可能成为可以对话的合作者，而不是只吐结果的黑箱。对工程团队来说，研究图提供了一种管理长程多智能体任务的思路：用结构化的外部记忆替代不断膨胀的上下文，让智能体跨会话也能接上之前的工作。这个思路并不限于数学，可以迁移到其他需要长期推理和可审计性的场景，比如形式化验证、科学计算和代码审查。对开源社区和后续研究，这篇论文留下了几个值得追的问题：研究图的结构如何标准化，验证证据如何与形式化证明工具对接，团队状态回放在多人协作时如何处理分歧。同时也要保持谨慎，摘要没有给出定量结果，实际效果还有待更多用户研究和独立复现来检验。