发表机构
University of California, Los Angeles（加利福尼亚大学洛杉矶分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出Ansatz，一个基于持续图记忆的数学研究智能体，通过统一图结构组织证明搜索过程并重用跨问题知识，在十个研究任务上实现闭合，并自主解决多个开放数学问题。
AI 中文摘要
利用前沿智能体框架来解决数学研究问题已成为推动数学发展的有效手段。然而，解决数学中的前沿问题可能需要大量智能体并行工作较长时间来构造证明，从而产生海量的中间证明结果。在整个长时程证明搜索过程中组织这些中间结果，并重用先前探索中获得的知识，仍然是主要挑战。我们提出了Ansatz，一个围绕持续图记忆构建的数学研究智能体，持续图记忆是一种基于图、可演化、跨问题的数学研究记忆系统，它显式地组织整个证明搜索过程，并重用先前问题探索轨迹中的信息。具体来说，我们开发了一个统一的图记忆，表示所有中间探索结果，包括事实、计划和反例，以及显式表示它们之间关系的边；依赖感知检索提供精确的目标局部上下文；证据敏感的策展器更新研究前沿并从先前尝试中提炼经验教训；作用域召回呈现早期陈述和负面发现用于局部重新证明，而非不加批判地重用。实验涵盖所有十个First Proof Second Batch问题的运行，以及四项组件研究。Ansatz报告在所有十个研究任务上完成闭合，展示了其维持和恢复长时程数学搜索的能力。除了这些问题，Ansatz还在无需人工干预的情况下解决了Jamison caterpillar猜想和Erdős问题289、348和488，并在几个开放问题上取得了部分进展，展示了其解决开放数学研究问题的强大能力。
英文摘要
Using frontier agent harnesses to tackle mathematical research problems has emerged as an effective means of advancing mathematics. However, solving frontier problems in mathematics may require a massive number of agents working in parallel for extended periods to construct proofs, thereby generating an enormous volume of intermediate proof results. Organizing these intermediate results throughout a long-horizon proof-search process and reusing knowledge gained from prior explorations remain major challenges. We present Ansatz, a mathematical research agent built around Continual Graph Memory, a graph-based, evolvable, cross-problem mathematical research memory system that explicitly organizes the entire proof search process and reuses information from exploration trajectories of previous problems. Specifically, we develop a unified graph memory that represents all intermediate exploration results, including facts, plans, and counterexamples, together with edges that explicitly represent the relationships among them; dependency-aware retrieval supplies precisely targeted local context; an evidence-sensitive curator updates the research frontier and distills lessons from prior attempts; and scoped recall surfaces earlier statements and negative findings for local re-proving rather than uncritical reuse. Experiments cover runs across all ten First Proof Second Batch problems, together with four component studies. Ansatz reports closure on all ten research tasks, demonstrating its ability to sustain and resume long-horizon mathematical search. Beyond these problems, Ansatz also produces solutions to the Jamison caterpillar conjecture and Erdős Problems 289, 348, and 488 without human intervention, and makes partial progress on several open problems, illustrating its strong ability to solve open mathematical research problems.
