研究人员提出了 Danus，这是一种用于研究级数学推理的编排系统，它利用共享的事实图作为全局内存管理机制。该系统协调一个负责规划的主智能体和多个执行并行证明搜索的工作智能体，并使用无状态验证器在声明进入图之前检查其有效性。

  • Danus 存储经过验证的事实及其证明和逻辑依赖关系，以逐步构建长论证，同时保持共享证明状态的有序性。
  • 主智能体定期总结不断演变的证明状态，将工作智能体重定向到有希望的方向，并通过进度报告支持与人类数学家的交互。
  • 通过对代数几何、奇点理论和组合学中的六个研究级案例研究进行评估，展示了事实图机制如何 enables 构建长而详细的数学证明。

结果表明，基于事实图的编排为扩展用于长期研究问题的数学推理智能体提供了一条有效途径。