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.
Figures & tables
Figure 1: Continual Graph Memory. (a) The harness consists of workers, strategy consultation, and verifiers. The graph memory system coordinates the exploration process of all agents. Agents update and access the memory through tool calls. (b) Dependency-aware retrieval leverages the dependency information in the graph to provide multi-hop information about the target theorem. (c) Curator organizes the whole graph, update node states based on edge-based information propagation, revisits stale annotations and record structured lessons at orderly project close. (d) Scoped recall retrieves fact statements, negative findings, and methodological lessons together with provenance. The twenty most recent eligible lessons are included in the context of a later curator. Cross-project statements must be re-admitted locally under the agent protocol, while temporal isolation requires sequential orchestration.
Official Participating Team
Our Reported results
Task
ETH
UCLA
OpenAI
Princeton
Plain
Codex
Danus
Ansatz
LLM
GPT-5.5 Pro ‡
GPT-5.5 Pro
GPT-5.5 Pro
Gemini 3.1 Pro Preview
GPT-5.6 Sol
GPT-5.6 Sol
GPT-5.6 Sol
GPT-5.6 Sol
01 Automorphism
✓
✓
✓
×
✓
✓
✓
✓
02 Möbius
✓
✓
✓
×
✓
✓
✓
✓
03 Bernoulli
✓
×
×
×
×
×
×
✓
04 Dilation
×
×
×
×
×
×
×
✓
Table 1: Experimental results for First Proof Second Batch. ✓ : Pass (essentially flawless or minor revisions); △ : major revisions; × : reject; —: no submission. ‡ ETH additionally calls GPT-5.5, Gemini 3.1 Pro Preview, Claude Opus 4.7.
Figure 3: (a) Memory retrieval activity across First Proof Second Batch tasks. The bars report the number of memory retrieval calls made by Ansatz for each task. Blue denotes calls to the embedding-based memory_recall tool, while green denotes calls to the graph-based multi-hop fact_neighbors tool. (b) Independent verifier review of selected records approved by workers through self-review. Bar labels indicate rejected/reviewed counts. We use a census for Tasks 01 and 06 and random sampling for Tasks 03 and 10.
Component study
01
02
03
05
06
07
08
09
10
Closed
A. Flat fact notebook
✓
✓
—
✓
✓
✓
✓
✓
—
7/7
B. No exploration graph or curator
✓
✓
—
×
✓
✓
✓
✓
—
6/7
C. Worker self-review
✓
—
×
—
✓
—
—
—
×
2/4
D. No strategy consult
✓
—
×
—
×
—
—
—
×
1/4
Ansatz
✓
✓
✓
✓
✓
✓
✓
✓
✓
10/10
Table 2: Ablation study of the components in Ansatz. Since conducting ablation studies of Ansatz on research-level tasks is very costly, we selected seven problems for ablation studies A and B, and four problems for ablation studies C and D.
#289 Erdős–Graham interval problem [ Erdős and Graham, 1980 ]
Open [ Bloom, 2026b ]
all large k
all large k
Solved
#488 density of multiples [ Bloom, 2026e ]
Open [ Bloom, 2026e ]
counterexample; ratio >256/67
decide factor- 2 bound
Solved
#348 complete-sequence deletion problem [ Erdős and Graham, 1980 ]
m=0,1 known [ Bloom, 2026d ]
exactly m=0,1
classify all m<n
Solved
#811 balanced-rainbow problem [ Erdős and Tuza, 1993 ]
most q [ Axenovich and Clemen, 2024 ] ; K4 [ Clemen and Wagner, 2023 ]
cliques q≥4
all graphs
Partial
#644 pair-transversal conjecture [ Erdős et al., 1992 ]
7/8 [ Fon-Der-Flaass et al., 1999 ]
6/7
3/4
Partial
Table 3: Ansatz outcomes on open problems. Solved indicates that the target is met, while Partial indicates meaningful progress toward the target without fully meeting it.
Autonomous research agents use language models and tools to search literature, design and run experiments, analyze results, and support scientific discovery.
Recent LLM-based mathematical reasoning agents have begun to tackle research-level problems and, in several cases, have contributed to the resolution of open problems. However, scaling and orchestrating such agents effectively remains challenging, due to the difficulty of coordinating parallel proof search while keeping intermediate claims organized and reliable. In this paper, we propose Danus, an orchestration system for research-level mathematical reasoning centered on a shared fact graph as a global memory-management mechanism. Danus consists of a main agent that performs planning and coordination, multiple worker agents that carry out proof search in parallel, and a stateless verifier that checks proposed mathematical claims before they are admitted into the fact graph. Each verified fact is stored together with its proof and logical dependencies, allowing the system to build long arguments incrementally while keeping the shared proof state organized. The main agent periodically summarizes the evolving proof state, redirects workers across promising directions, and supports interaction with human mathematicians through progress reports. We evaluate Danus through six research-level case studies in algebraic geometry, singularity theory, and combinatorics, illustrating how the fact-graph memory mechanism enables Danus to construct long, detailed mathematical proofs. Our results suggest that fact-graph-based orchestration provides an effective route toward scaling mathematical reasoning agents for long-horizon research problems. Danus is open source at https://github.com/frenzymath/Danus.
Jihao Liu, Guoxiong Gao, Zeming Sun +8
School of Mathematical Sciences, Peking University · Beijing International Center for Mathematical Research, Peking University · Research Institute for Mathematical Sciences, Kyoto University +8
Mathematical research drives scientific discovery, and recent advances in AI for mathematics have shown that language-model agents can solve challenging problems and develop substantial mathematical proofs. Yet much of today's AI-for-mathematics work centers on obtaining a final answer. This emphasis leaves the exploration behind a result difficult for researchers to understand, while long-running investigations face fragmented context and the risk of unsupported claims propagating across reasoning steps. We present Euler, a human-centered mathematical research system built around a shared, structured representation of the research process. Euler organizes mathematical statements, assumptions, proof dependencies, alternative approaches, failed attempts, and verification evidence into connected research graphs. This representation allows researchers to trace how results are developed and supplies agents with persistent, task-relevant knowledge for planning, collaboration, and verification across sessions. Researchers can also select a graph node linked to a saved team state, revisit the agents' earlier reasoning, and explore alternative directions through continued interaction. We illustrate Euler's capabilities through three mathematical research case studies and describe the implemented system and its software validation.
Qiuyu Chen, Qi Wang, Liang Xu +3
Shanghai Jiao Tong University · Ningbo Key Laboratory of Spatial Intelligence and Digital Derivative, Ningbo Institute of Digital Twin, Eastern Institute of Technology, Zhejiang, China · Institute of Automation, Chinese Academy of Sciences +1
Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and expose the right semantic state across many iterations. Left unmanaged, this produces research-level proofs that are locally convincing yet globally incomplete: a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents (RMA), an agentic framework for long-horizon proof development built around a persistent, typed research store and an orchestrator that compiles operation-specific context from that store. The Research Context Orchestrator is the central state-management layer between the persistent research store and each locally scoped proof operation: it retrieves task-relevant artifacts, compiles them into a bounded context, invokes the appropriate operation, and writes the resulting proof edits, issue updates, literature notes, plans, or evaluations back to the store. This process is designed to keep proof revisions, unresolved issues, prior attempts, literature, and evaluations available across rounds while exposing only task-relevant state to each local operation. We evaluate RMA across complementary research-level settings using independent expert evaluation, blind mathematician review, LLM-based benchmark evaluation, and Lean 4 kernel verification. RMA achieves a 42.5% solve rate on the independently evaluated SOOHAK Challenge Hard set, obtains 8 of 10 correct solutions on First Proof B1 and 8 of 10 passing solutions on B2 under human-expert evaluation, and verifies 213 of 300 sampled Research Solved targets in Formal Conjectures with the Lean 4 kernel.