Continual Graph Memory for Mathematical Research Agents
Junyi Zhang, Jinxi Yu, Eric Hanchen Jiang and colleagues at UCLA, with senior authors including Kai-Wei Chang, Raghu Meka, Nanyun Peng, Amit Sahai, Terence Tao and Wei Wang, present Ansatz, a mathematical research agent built around Continual Graph Memory, which stores proof progress as typed graphs instead of flat text.
Ask this paper
Memory design. Ansatz keeps three linked stores: a project-local dependency graph of accepted proof records, a typed exploration graph of facts, plans and counterexamples, and structured lessons written by a curator at project close. A separate verifier controls which facts are admitted.
Retrieval. Dependency-aware neighborhood retrieval gives each worker only the lemmas a target theorem depends on, and scoped recall exposes results from earlier projects only as candidates to be re-proved locally, never as trusted facts.
Benchmark result. Ansatz reports local closure on all ten First Proof Second Batch problems, more than Danus or any of the four expert-reviewed baselines. The authors note that several factors changed at once, so the extra closures cannot be credited to memory alone.
Open problems. Without human intervention, Ansatz produces complete solutions to the Jamison caterpillar conjecture and ErdÅs Problems 289, 348 and 488, and makes partial progress on six more open problems.
Abstract
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.