Continual Graph Memory for Mathematical Research Agents

Continual Graph Memory for Mathematical Research AgentsThanks: Senior authors served as equal advisors and are listed alphabetically.

   Jinxi Yu ^*    Eric Hanchen Jiang ^*    Jiachen Lu    Zhi Zhang Affiliation: Xinjie He, Hyunsik Chae, Ethan Ji, Alexander K Taylor, Vigyan Sahai, Affiliation: Yiwen Kou, Kai-Wei Chang , Raghu Meka ²²footnotemark: 2 , Nanyun Peng ²²footnotemark: 2 , Amit Sahai ²²footnotemark: 2 , Affiliation: Terence Tao ²²footnotemark: 2 , Wei Wang ²²footnotemark: 2 Affiliation: [1em] University of California, Los Angeles

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. Our code and results are available at https://github.com/uclanlp/continual-graph-memory

^††footnotetext:

1 Introduction

Mathematical research is not a sequence of isolated proofs. Difficult problems generate partial reductions, failed constructions, useful counterexamples, promising analogies, and lemmas whose significance may become clear only much later. Language-model agents can already explore multiple lines of reasoning through stepwise inference and sampled solution paths [Wei et al., 2022; Wang et al., 2023b], while research-oriented systems such as Danus and Albilich extend this process with parallel workers, persistent proof state, and verification [Liu et al., 2026; Gong et al., 2026]. But persistence alone is not enough. A research agent must decide what to remember, retrieve, trust, and reuse. These memories serve different roles: a method suggests what to try, a lemma is valid only when its assumptions hold, and a plan records a search choice rather than a proven fact. Treating them all as the same kind of text hides their evidential status and reuse conditions. This is especially risky for LLMs, which may store a flawed intermediate argument and later propagate the error through persistent memory.

We introduce Ansatz, a mathematical research agent built around Continual Graph Memory, an evolvable memory architecture designed to preserve these distinctions. Continual Graph Memory combines three complementary forms of memory: a project-local dependency graph of accepted proof records, a typed exploration graph connecting facts, plans, and counterexamples, and many other intermediate findings. An evidence-sensitive curator updates the exploration frontier and records reusable experience, while a separate verifier controls the admission of ordinary mathematical facts. Dependency-aware neighborhood retrieval supplies only locally relevant context, and scoped recall exposes potentially useful material from eligible prior projects for local re-proving rather than unconditional reuse. Figure 1 summarizes this interaction.

We evaluate Ansatz on all ten problems from First Proof Second Batch [Abouzaid et al., 2026]. Ansatz reports local closure on all ten tasks. We compare these outcomes with those of Danus and the four expert-reviewed baselines reported in the benchmark publication. Ansatz reports local closure on more tasks than any of these comparison methods. Because these factors vary simultaneously, the additional closures cannot be attributed to memory alone. We therefore complement task-level outcomes with matched resource and memory diagnostics from the earlier configuration, four component studies, and post-hoc review of accepted records to study how memory is allocated, retrieved, and occasionally misused.

Beyond First Proof Second Batch [Abouzaid et al., 2026], we further evaluate Ansatz in open-ended mathematical research settings on a collection of difficult open problems. Ansatz produces complete solutions to four problems, including the Jamison caterpillar conjecture and Erdős Problems 289, 348, and 488, without human intervention, and makes meaningful progress toward the targets on six additional problems. These experiments test whether Ansatz can sustain long-horizon mathematical search beyond benchmark-style tasks. Taken together, the results suggest that the system is capable not only of partial progress on challenging open problems, but also of independently reaching complete solutions.

Our contributions are: (1) An graph-based, evolvable and cross-problem memory architecture for mathematical research. We introduce a structured memory system that separates certified proof records, exploratory state, and cross-project experience, combining dependency-aware local retrieval, evidence-sensitive curation, and scoped recall under explicit admission boundaries. (2) An auditable empirical study of persistent mathematical research. We report complete task-level results on First Proof Second Batch, comparisons with published expert-reviewed baselines, matched resource and memory diagnostics, four component studies, and open-ended research cases study together with explicit verification qualifications and the full proof artifact. (3) Real Advances in Mathematics. We allocate resources to run Ansatz on dozens of open problems in mathematics and have successfully tackled or partially solved several problems at the frontier of mathematics, leading to genuine advances in the field.

2 Related Work

Proof search and orchestration.

Language-agent systems interleave reasoning with tool use [Yao et al., 2023b] and explore branching or graph-structured reasoning trajectories [Yao et al., 2023a; Besta et al., 2024]. For mathematical research, Rethlas and Archon combine informal conjecture resolution with a separate formalization stage [Ju et al., 2026]. Danus introduces the immediate architectural foundation for our work: parallel workers, a stateless verifier, and a shared graph of accepted facts with explicit proof dependencies [Liu et al., 2026]. Albilich likewise organizes long-horizon research around persistent proof state, verification, human steering, and computer algebra [Gong et al., 2026]. Our work builds a unified graph memory that targets the proof-search process for mathematical research problems, represents the detailed relationships among different types of intermediate proving information rather than facts alone, and enables cross-problem learning and reuse of the graph memory.

Evolving agent memory.

Reflexion stores linguistic feedback from prior attempts [Shinn et al., 2023], Voyager accumulates reusable executable skills [Wang et al., 2023a], and MemGPT manages information across memory tiers [Packer et al., 2023]. More recent systems make memory organization itself adaptive: A-MEM links and evolves structured notes [Xu et al., 2025], Mem0 extracts and consolidates conversational memories, including a graph-based variant [Chhikara et al., 2025], and G-Memory connects insights, queries, and multi-agent interaction histories [Zhang et al., 2025]. ISM is especially close in its use of an actively maintained strategy bank for mathematical reasoning with a frozen model and symbolic verification [Dixit and Oates, 2026]. CoEvoSkills couples evolving skill packages with an independent surrogate verifier that supplies revision feedback [Zhang et al., 2026]. Our work systematically studies evolving memory for mathematical research tasks and integrates it into a mathematical research system.

Continual Graph Memory is the memory layer of Ansatz. It fixes what an agent may store, who may write to each store, how stored material is retrieved, and what carries over to the next problem. This section gives the intuition; exact definitions, defaults, and algorithms are in Appendix A.

3.1 Overview

Ansatz works through a sequence of research problems. Each problem is a project with a task statement and a compute budget. Within a project, many worker sessions start and end, so progress must live outside any single context window. Across projects, experience should transfer, but a statement proved in an earlier project must not count as proved in the current one.

Several LLM roles act on shared memory through tools. Workers explore and write proofs. A verifier reviews each submitted proof in a fresh session. A curator reads the exploration state and scores which routes look promising. A main agent assigns workers to routes, requests strategy consultations, and decides when to stop.

3.2 Admitting facts

A worker submits a candidate through fact_submit: a statement, a proof, and the identifiers of the accepted facts the proof relies on. The candidate becomes a fact only if three steps all succeed. First, deterministic prechecks reject vacuous content, known unsupported proof patterns, and any cited predecessor that has been revoked. Second, a fresh verifier session reads the statement and proof and returns correct, or wrong with repair hints. Third, the fact store writes the record and returns its identifier. Each fact gets a content-addressed identifier, so resubmitting the same statement and proof yields the same record. One dependency edge is recorded from each cited predecessor. Because this is the only path into the fact graph, curator scores, discussion posts, and recalled statements can never become accepted facts on their own.

If an accepted fact is later found faulty, fact_revoke removes it together with every fact that declared it as a dependency, and logs the decision. Throughout the paper, “accepted” means accepted by an LLM verifier, not checked by a proof assistant.

3.3 Organizing exploration

Typed exploration graph.

Most of a research run consists of attempts rather than proofs. Workers record attempts as nodes such as plans, findings, goals, counterexamples, and obstacles, and connect them to each other and to facts with graph_link, choosing from fourteen relation types such as decomposes-into, refutes, and promoted-to. A dependency edge in the fact graph says “this proof uses that fact”; an exploration edge only says “these two are related in this way.”

Curator annotations.

Through graph_annotate, the curator attaches to a node a status (such as open, active, closed, dead, or blocked), an optional score in [0,1], the evidence it read, and a short rationale. Annotations are appended, and the latest one is the node’s current view. The curator’s contract says when a route may be marked closed: a decomposition closes its parent only when every obligation, including any reassembly step, is closed; a reduction needs an accepted bridge; an equivalence needs both directions. These rules are prompt instructions; the store only checks relation types and score ranges (Section A.3).

Frontier and staleness.

graph_frontier returns a ranked worklist of open routes: linked nodes before unlinked, scored before unscored, higher scores first. If a node gains a new edge after its last annotation, that annotation is flagged stale and the curator revisits it. Judgments therefore stay tied to the evidence that existed when they were made.

3.4 Retrieving context

A fresh worker session cannot read every earlier interaction, so it retrieves (Section A.4). fact_search ranks stored statements with BM25 [Robertson and Zaragoza, 2009] and returns matching identifiers and statements. fact_neighbors then starts from one fact and returns its declared predecessors, optionally its direct dependents, and the accepted facts that share an exploration edge with it or sit two edges away through a non-fact node, together with the connecting paths and edge labels. In Figure 1b, a query for f3 returns its predecessors f1,f2 and also f4, which shares no words with f3 but supports the same goal g. The default budget is 25 statements, predecessors first. Both tools return statements, not proofs; the worker decides what to read and what to reuse.

3.5 Carrying experience across projects

Scope.

An operator setting decides which other projects are visible: off (none, the default), batch (projects sharing the current batch label), or all. Scope filters by membership, not by time. An evaluation in which only earlier projects should be visible must enforce that ordering outside the memory system (Section A.5).

Recall.

memory_recall searches three channels separately with BM25—fact statements, negative findings (dead ends, obstacles, counterexamples), and lessons—and returns five results per channel by default, each tagged with its source project. A recalled fact arrives as a statement without a proof and has no standing in the current project. A worker who wants to use it must re-prove it and submit it through fact_submit like any other candidate. Negative findings help workers avoid repeating known failures.

Lessons.

When a project closes in an orderly way, the curator may call lesson_add with a pattern it noticed in its own scoring, the outcome evidence, and a proposed adjustment. The next project’s curator starts with the twenty most recent eligible lessons in its context; workers and the main agent query lessons on demand. Adaptation across projects thus happens in inspectable text rather than in model weights.

4 Experiments

Our experiments consist of two parts. In Section 4.1, we evaluate Ansatz on the First Proof Second Batch benchmark. Since this is a research-level mathematics benchmark for which solutions are publicly available, we disable Ansatz’s web search functionality to prevent access to existing solutions. In Section 4.2, we evaluate Ansatz on genuinely open mathematical problems and report several results obtained by Ansatz on these problems.

4.1 First Proof Benchmark

4.1.1 Experimental setup

We use all ten problems from the First Proof Second Batch [Abouzaid et al., 2026] as our evaluation set. Since First Proof Second Batch is a research-level mathematics benchmark whose solutions have already been made public, we disable the web search functionality of the agent systems during our new evaluations. We report results for Ansatz, Danus, Codex, and plain GPT-5.6 Sol, all using GPT-5.6 Sol as the base model. We compare these results against those of the four teams included in the official First Proof Second Batch report.

4.1.2 Performance of Ansatz

Experimental results for First Proof Second Batch are shown in Table 1. Ansatz substantially outperforms both the official participating teams and the other GPT-5.6-based baselines on the First Proof Second Batch benchmark. Ansatz solves all 10/10 tasks, achieving the highest overall pass rate among all evaluated systems, compared with 7/10 for Danus, 6/10 for Codex, and 4/10 for the plain GPT-5.6 solution, as well as 6/10, 5/10, 5/10, and 1/10 for the four official participating teams. The gains are particularly pronounced on problems for which most other systems fail. In particular, Ansatz is the only system in the table to pass Task 04 (Dilation) and the only system to pass Task 10 (von Neumann): all other systems are rejected on Dilation, while the best official submissions on von Neumann require major revisions. Ansatz also passes Task 03 (Bernoulli), where all systems except the ETH submission fail, as well as Tasks 05 (SPDE), 06 (Tree-lattice), and 08 (Dressian), on which multiple competing systems fail or require major revisions. These results suggest that the gains from Ansatz cannot be explained by the GPT-5.6 backbone alone. With the same GPT-5.6 Sol backbone, Ansatz improves over the plain baseline from 4/10 to 10/10, while also outperforming Codex (6/10) and Danus (7/10), indicating that the proposed system design substantially improves performance across a diverse set of research-level mathematical problems.

4.1.3 Memory activity and evidence reuse

The memory retrieval activity across First Proof Second Batch tasks is shown in Figure 3(a). Memory activity varies substantially across tasks, while graph-based retrieval consistently accounts for the majority of memory accesses. fact_neighbors is invoked more frequently than the embedding-based memory_recall tool on every Second Batch problem, indicating that the agent frequently expands retrieved facts through multi-hop graph traversal rather than relying solely on embedding-based similarity search. The difference is particularly pronounced on Task 05 (SPDE), where the system makes 343 fact_neighbors calls, together with a large number of memory_recall calls, indicating substantially more intensive memory exploration than on the other tasks. Tasks 03, 04, and 06 also trigger relatively high levels of graph traversal, whereas Tasks 01, 02, and 10 involve comparatively little memory interaction. The substantial variation across tasks suggests that Ansatz does not operate with a fixed retrieval budget, but instead adjusts its memory activity to the course of reasoning on each problem. Notably, Ansatz successfully solves all ten tasks despite large differences in retrieval volume: for example, Task 05 requires intensive memory interaction, whereas Task 10 is solved with relatively few retrieval calls. Thus, retrieval frequency alone is not indicative of end-task success; rather, the amount of memory exploration required can vary considerably across problems.

4.1.4 Component Ablation

The ablation study of the components in Ansatz is shown in Table 2. For the seven tasks used in ablations A and B, the full Ansatz system succeeds on all seven. Replacing the fact graph with a flat fact notebook (A), while preserving the stored facts but removing graph edges, retains the same 7/7 success rate. Thus, on this subset, the explicit graph structure of the fact memory does not yield an observable improvement in end-task performance. In contrast, removing the exploration graph and curator (B) introduces a failure on Task 05, reducing performance from 7/7 to 6/7 and providing evidence that the exploration-and-curation mechanism contributes to successful problem solving.

For ablations C and D, we evaluate four tasks (01, 03, 06, and 10), all of which are solved by the full Ansatz system. Replacing the independent verifier with worker self-review (C) introduces failures on Tasks 03 and 10, reducing performance from 4/4 to 2/4. Removing strategy consultation (D) has an even larger effect, introducing failures on Tasks 03, 06, and 10 and leaving only Task 01 solved, for an overall success rate of 1/4.

Figure 3(b) reports an independent re-review of records that had previously been accepted by workers through self-review. The audit further reveals a weakness of relying on workers to verify their own outputs: among 80 records accepted by worker self-review, 7 are subsequently rejected by an independent reviewer. The rejected records are concentrated most heavily on Task 10, where 5 of 21 accepted records fail independent review; one rejected record is also found on each of Tasks 01 and 03, while none are found among the 15 reviewed records for Task 06. Notably, the self-review ablation fails on Tasks 03 and 10, both of which contain records that were accepted by worker self-review but rejected upon independent re-review. This correspondence does not by itself establish that these records caused the end-task failures, but it provides direct evidence that worker self-review can admit erroneous intermediate facts. Task 10 is particularly informative, as it exhibits both the highest rate of independently rejected records and an end-task failure under the self-review ablation.

Overall, these results provide evidence for the practical value of the exploration-and-curation mechanism, independent verification, and strategy consultation. In contrast, we do not observe a measurable benefit from the fact-graph structure itself in this ablation, suggesting that, for the tasks studied here, how facts are explored, validated, and used strategically may matter more than whether they are stored with explicit graph edges.

4.2 Open Problems

Here we run the same system on open problems. Table 3 records the published current best, the Ansatz claim, the conjectured target, and whether that claim solves the problem. Ansatz produces complete solutions to four mathematical problems: the Jamison caterpillar conjecture and Erdős Problems 289, 488, and 348, without human intervention. Ansatz also makes meaningful progress toward the targets on six additional problems. The statements of the four solved problems are shown below, while the statements of the other problems are provided in Appendix  B.

Jamison.

The mean subtree order of a tree is the average order of its nonempty connected induced subgraphs. Jamison conjectured that every n-vertex maximizer is a caterpillar [Jamison, 1983; Jamison, 1984]. Mol and Oellermann verified this through n=24 and restricted the limbs of any maximizer [Mol and Oellermann, 2019]. Ansatz proves that every n-vertex maximizer is a caterpillar: a shortest terminal arm is reduced to a broom, then straightened by exact polynomial certificates. This fully solves the conjecture for every n.

289.

Erdős and Graham asked whether 1 can be written as a sum of reciprocals over k finite intervals of positive integers, for every sufficiently large k [Erdős and Graham, 1980; Bloom, 2026b]. The catalogue form requires the intervals to be pairwise disjoint and non-adjacent, each of length at least two; that separated form was open. Ansatz produced a proof that such a threshold k0 exists. The argument uses a Pell anchor, equal-mass packets, and a summable reserve; the threshold is not effective, because the last step uses compactness. The unrestricted variant, which allows overlap, already has a short affirmative argument [Kovač, 2025].

488.

For a finite nonempty set A of positive integers, let B be the set of their multiples and write dA​(t)=|B∩[1,t]|/t. Erdős asked whether dA​(m)<2​dA​(n) whenever m>n≥max⁡A [Bloom, 2026e]. Ansatz constructs a finite A and admissible m,n with dA​(m)/dA​(n)>256/67>2, disproving the inequality. Its elements have prime factors in a fixed finite set and are at least a threshold, but division by any prime factor puts them below it. Their multiples have low density near max⁡A, while an exact residue-class count gives a higher density at a later cutoff.

348.

A sequence is complete if every sufficiently large positive integer is a sum of terms at distinct indices; repeated values are allowed. The question asks which 0≤m<n admit a sequence that stays complete after every m-term deletion but becomes incomplete after every n-term deletion [Erdős and Graham, 1980; Bloom, 2026d]. The cases m=0,1 were known; van Doorn excluded m≥2 under the stronger definition requiring every positive integer to be represented [Bloom, 2026d]. Ansatz proves that, under eventual completeness, the admissible pairs are exactly (0,n) for n≥1 and (1,n) for n≥2. Powers of two and the Fibonacci sequence supply the two families. For the converse, Ansatz proves that any sequence surviving every two-term deletion admits a deletion of any prescribed finite size that preserves completeness, ruling out m≥2.

For the Jamison caterpillar conjecture, our result is, to the best of our knowledge, the first complete resolution of the conjecture. For the other three solved problems: Erdős–Graham Problem 289, Problem 488 on the density of multiples, and Problem 348 on complete-sequence deletion, we found, after the Ansatz runs had been completed, that recent proofs had also been obtained by other groups. However, a post hoc audit of the complete retrieval and reasoning traces showed that Ansatz did not retrieve, access, or rely on these contemporaneous proofs while solving the problems. Its solutions were derived independently from the information available during the runs. Moreover, the resulting proofs use approaches that are materially different from those in the contemporaneous solutions. Taken together, these results indicate that Ansatz is capable not only of making partial progress on difficult open problems, but also of independently reaching complete solutions, demonstrating its strong capability in real-world mathematical research.

To enable independent verification of these claims and facilitate further study, we will publicly release the complete run artifacts and results for all ten problems, including the retrieval and tool-use records, intermediate outputs, and final solutions. This release will make it possible to inspect not only the final mathematical results but also the computational provenance of each run, including the information retrieved and used during problem solving. We believe that this will make our results transparent, publicly accessible, and reproducible.

5 Conclusion

In this paper, We present Ansatz, a mathematical research agent built around Continual Graph Memory, a graph-based and evolvable memory system for persistent mathematical reasoning. By preserving and organizing intermediate progress, failed attempts, and reusable insights, Ansatz supports sustained proof search across long reasoning trajectories. Across the ten First Proof Second Batch problems, Ansatz closes all ten tasks. It also produces solutions to the Jamison caterpillar conjecture and Erdős Problems 289, 348, and 488 without human intervention, showing the potential of structured research memory beyond benchmark problems. Our results suggest that representing the proof-search process in a graph-based memory, enabling cross-problem learning, and continuously evolving the memory provide an effective way to support long-horizon mathematical problem solving and move mathematical research agents toward sustained exploration.

References

• Abouzaid et al. (2026) M. Abouzaid, N. Srivastava, R. Ward, and L. Williams First proof second batch. External Links: 2606.18119, Link Cited by: §1, §1, §4.1.1.
• Axenovich and Clemen (2024) M. Axenovich and F. C. Clemen Rainbow subgraphs in edge-colored complete graphs: answering two questions by Erdős and Tuza. Journal of Graph Theory. Note: Also arXiv:2209.13867 Cited by: Appendix B, Table 3.
• Basit and Galvin (2021) A. Basit and D. Galvin On the independent set sequence of a tree. Electronic Journal of Combinatorics 28 (3). Note: arXiv:2006.12562 Cited by: Appendix B, Table 3.
• Besta et al. (2024) M. Besta, N. Blach, A. Kubíček, R. Gerstenberger, M. Podstawski, L. Gianinazzi, J. Gajda, T. Lehmann, H. Niewiadomski, P. Nyczyk, and T. Hoefler Graph of thoughts: solving elaborate problems with large language models. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 38, pp. 17682–17690. External Links: Document, Link Cited by: §2.
• Bloom (2026a) T. F. Bloom Erdős Problem #1063. Note: https://www.erdosproblems.com/1063Accessed 26 September 2026 Cited by: Appendix B.
• Bloom (2026b) T. F. Bloom Erdős Problem #289. Note: https://www.erdosproblems.com/289Accessed 25 September 2026 Cited by: §4.2, Table 3.
• Bloom (2026c) T. F. Bloom Erdős Problem #302. Note: https://www.erdosproblems.com/302Accessed 26 September 2026 Cited by: Appendix B.
• Bloom (2026d) T. F. Bloom Erdős Problem #348. Note: https://www.erdosproblems.com/348Accessed 26 September 2026 Cited by: §4.2, Table 3.
• Bloom (2026e) T. F. Bloom Erdős Problem #488. Note: https://www.erdosproblems.com/488Accessed 26 September 2026 Cited by: §4.2, Table 3, Table 3.
• Bloom (2026f) T. F. Bloom Erdős Problem #561. Note: https://www.erdosproblems.com/561Accessed 25 September 2026 Cited by: Appendix B.
• Bloom (2026g) T. F. Bloom Erdős Problem #644. Note: https://www.erdosproblems.com/644Accessed 25 September 2026 Cited by: Appendix B.
• Bloom (2026h) T. F. Bloom Erdős Problem #811. Note: https://www.erdosproblems.com/811Accessed 25 September 2026 Cited by: Appendix B.
• Bloom (2026i) T. F. Bloom Erdős Problem #993. Note: https://www.erdosproblems.com/993Accessed 24 September 2026 Cited by: Appendix B, Table 3.
• Burr et al. (1978) S. A. Burr, P. Erdős, R. J. Faudree, C. C. Rousseau, and R. H. Schelp Ramsey-minimal graphs for multiple copies. Indagationes Mathematicae 40, pp. 187–195. Cited by: Appendix B, Table 3.
• Chhikara et al. (2025) P. Chhikara, D. Khant, S. Aryan, T. Singh, and D. Yadav Mem0: building production-ready AI agents with scalable long-term memory. External Links: 2504.19413, Link Cited by: §2.
• Clemen and Wagner (2023) F. C. Clemen and A. Z. Wagner Balanced edge-colorings avoiding rainbow cliques of size four. Electronic Journal of Combinatorics 30 (3), pp. #P3.17. Cited by: Appendix B, Table 3.
• Davoodi et al. (2025) A. Davoodi, R. Javadi, A. Kamranian, and G. Raeisi On a conjecture of Erdős on size Ramsey number of star forests. Ars Mathematica Contemporanea. Note: Paper No. 9 Cited by: Appendix B, Table 3.
• Dixit and Oates (2026) P. Dixit and T. Oates ISM: self-improving strategy memory for continual mathematical reasoning. External Links: 2606.31191, Link Cited by: §2.
• Erdős et al. (1992) P. Erdős, D. Fon-Der-Flaass, A. V. Kostochka, and Z. Tuza Small transversals in uniform hypergraphs. Siberian Advances in Mathematics 2, pp. 82–88. Cited by: Appendix B, Table 3.
• Erdős and Graham (1980) P. Erdős and R. L. Graham Old and new problems and results in combinatorial number theory. Monographies de L’Enseignement Mathématique, Vol. 28, L’Enseignement Mathématique, Geneva. Cited by: Appendix B, §4.2, §4.2, Table 3, Table 3, Table 3.
• Erdős and Selfridge (1983) P. Erdős and J. L. Selfridge Problem 6447. The American Mathematical Monthly, pp. 710. Cited by: Appendix B, Table 3.
• Erdős and Tuza (1993) P. Erdős and Z. Tuza Rainbow subgraphs in edge-colorings of complete graphs. In Quo Vadis, Graph Theory?, Annals of Discrete Mathematics, Vol. 55, pp. 81–88. Cited by: Appendix B, Table 3.
• Erdős Problem a Day (2026) Erdős Problem a Day #1063: A real upper-bound jump on nk—corrected after a reader caught us overclaiming it. Note: https://erdosproblemaday.com/day/1063-one-large-primeAI-generated report, 25 July 2026 Cited by: Appendix B, Table 3.
• Fon-Der-Flaass et al. (1999) D. G. Fon-Der-Flaass, A. V. Kostochka, and D. R. Woodall Transversals in uniform hypergraphs with property (7,2). Discrete Mathematics 207, pp. 277–284. Cited by: Appendix B, Table 3.
• Gong et al. (2026) T. Gong, M. R. Zeng, and Y. Yang Albilich: steerable proof-state orchestration for LLM-based mathematical research with CAS integration. External Links: 2607.27705, Link Cited by: §1, §2.
• Jamison (1983) R. E. Jamison On the average number of nodes in a subtree of a tree. Journal of Combinatorial Theory, Series B 35, pp. 207–223. Cited by: §4.2, Table 3.
• Jamison (1984) R. E. Jamison Monotonicity of the mean order of subtrees. Journal of Combinatorial Theory, Series B 37, pp. 70–78. Cited by: §4.2, Table 3.
• Ju et al. (2026) H. Ju, G. Gao, J. Jiang, B. Wu, Z. Sun, L. Chen, Y. Wang, Y. Wang, Z. Wang, W. He, P. Wu, L. Xiao, R. Liu, B. Dai, and B. Dong Automated conjecture resolution with formal verification. External Links: 2604.03789, Link Cited by: §2.
• Khanukov (2026) D. Khanukov Two-sided computer-assisted progress on Erdős Problem 302. Note: Unrefereed preprintVersion 0.2.0-preprint, 13 September 2026 External Links: Link Cited by: Appendix B, Table 3.
• Kovač (2025) V. Kovač Comment on Erdős Problem #289. Note: https://www.erdosproblems.com/forum/thread/28922 September 2025. Accessed 25 September 2026 Cited by: §4.2.
• Liu et al. (2026) J. Liu, G. Gao, Z. Sun, B. Wu, S. Liu, J. Jiang, H. Ju, L. Chen, R. Cheng, X. Zhang, and B. Dong Danus: orchestrating mathematical reasoning agents with fact-graph memory. External Links: 2607.06447, Link Cited by: §1, §2.
• Mol and Oellermann (2019) L. Mol and O. R. Oellermann Maximizing the mean subtree order. Journal of Graph Theory 91, pp. 326–352. Cited by: §4.2, Table 3.
• Monier (1985) J. Monier Problems and solutions: solutions of advanced problems: 6447. The American Mathematical Monthly, pp. 435–436. Cited by: Appendix B.
• Packer et al. (2023) C. Packer, S. Wooders, K. Lin, V. Fang, S. G. Patil, I. Stoica, and J. E. Gonzalez MemGPT: towards LLMs as operating systems. External Links: 2310.08560, Link Cited by: §2.
• rickyc (2026) rickyc Comment on Erdős Problem #1063. Note: https://www.erdosproblems.com/forum/thread/106326 June 2026. Accessed 26 September 2026 Cited by: Appendix B.
• Robertson and Zaragoza (2009) S. Robertson and H. Zaragoza The probabilistic relevance framework: BM25 and beyond. Foundations and Trends in Information Retrieval 3 (4), pp. 333–389. External Links: Document, Link Cited by: §A.4, §3.4.
• Shinn et al. (2023) N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao Reflexion: language agents with verbal reinforcement learning. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §2.
• Wang et al. (2023a) G. Wang, Y. Xie, Y. Jiang, A. Mandlekar, C. Xiao, Y. Zhu, L. Fan, and A. Anandkumar Voyager: an open-ended embodied agent with large language models. External Links: 2305.16291, Link Cited by: §2.
• Wang et al. (2023b) X. Wang, J. Wei, D. Schuurmans, Q. Le, E. Chi, S. Narang, A. Chowdhery, and D. Zhou Self-consistency improves chain of thought reasoning in language models. In International Conference on Learning Representations, External Links: Link Cited by: §1.
• Wei et al. (2022) J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le, and D. Zhou Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, Vol. 35. External Links: Link Cited by: §1.
• Xu et al. (2025) W. Xu, Z. Liang, K. Mei, H. Gao, J. Tan, and Y. Zhang A-Mem: agentic memory for LLM agents. In Advances in Neural Information Processing Systems, Vol. 38. External Links: Link Cited by: §2.
• Yao et al. (2023a) S. Yao, D. Yu, J. Zhao, I. Shafran, T. L. Griffiths, Y. Cao, and K. Narasimhan Tree of thoughts: deliberate problem solving with large language models. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §2.
• Yao et al. (2023b) S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao ReAct: synergizing reasoning and acting in language models. In International Conference on Learning Representations, External Links: Link Cited by: §2.
• Zhang et al. (2025) G. Zhang, M. Fu, K. Wang, F. Wan, M. Yu, and S. Yan G-Memory: tracing hierarchical memory for multi-agent systems. In Advances in Neural Information Processing Systems, Vol. 38. External Links: Link Cited by: §2.
• Zhang et al. (2026) H. Zhang, S. Fan, H. P. Zou, Y. Chen, Z. Wang, J. Zhou, C. Li, W. Huang, Y. Yao, K. Zheng, X. Liu, X. Li, and P. S. Yu CoEvoSkills: self-evolving agent skills via co-evolutionary verification. External Links: 2604.01687, Link Cited by: §2.

Appendix A Formal specification of Continual Graph Memory

This appendix collects the definitions, update rules, and algorithms behind the description in Section 3. Each equation describes what the implementation stores or computes, and the surrounding text records the boundary conditions and defaults that the main text omits. The subsections follow the order of Section 3.

A.1 Memory state and memory-conditioned execution

For project pj at event t, the persistent state is

Here Li is worker i’s private process log, C contains shared findings and their evidence, F indexes accepted proof records, and EF records their declared dependencies. The exploration overlay (EX,A) connects plans, findings, facts, and goals through typed relations and curator annotations. Local and shared logs are append-only; a deployment-level lesson sequence Λj persists beyond any one project. Shared discussion can contain tentative conclusions, counterexamples, plans, or obstacles; membership in C does not imply membership in F.

An active role r chooses actions using its contract, private interaction history hj,tr, and memory responses xj,tr that it has obtained through its permitted tools:

This notation describes tool-mediated execution: πθr is the role’s LLM policy, gj the task specification, and o the resulting observation. The model parameters θ remain fixed within a deployment; experimental deployments may use different base models. Algorithm 1 summarizes the project sequence, and Algorithm 2 specifies the memory operations it calls. Workers and the curator run asynchronously, so the event loop is a procedural summary rather than a synchronized round schedule.

A.2 Fact identifiers, admission, and revocation

A candidate f=(p,S,Π,P,G,B) contains a statement S, proof Π, predecessor identifiers P, glossary entries G, and bibliography metadata B. The fact store assigns

The identifier uses the first 64 hash bits. Canonicalization sorts predecessors and glossary entries and normalizes statement/proof whitespace, giving repeated canonical content the same identifier. Bibliography metadata is excluded so that citation corrections preserve dependency links; citation keys inside the proof remain hashed.

Workers submit through fact_submit. Let ht​(f) indicate that deterministic prechecks and the revoked-predecessor check pass, vt​(f) be the fresh verifier’s verdict, and wt​(f) indicate a completed fact write. Unexecuted or failed stages take a nonaccepting value. Acknowledged admission is

For an admitted candidate with u=id⁡(f), the update is

An edge (r,u) records a declared proof dependency. Deterministic checks reject vacuous content and selected unsupported proof patterns; glossary coverage is advisory. Once a verifier verdict exists, the gateway records the verdict, report, and any write failure in shared memory, and successful writes can link back to an originating finding. An accepting verdict without a returned fact identifier is not acknowledged admission. Equation (A.5) describes completed writes, not recovery from arbitrary I/O failures.

Proposition 1 (Local admission property).

Starting from an empty fact store, suppose all additions use the default gateway and persistence succeeds. Every admitted fact has an accepting verdict from a separate verification invocation. Changing curator scores alone cannot admit a fact.

The property follows from the gateway’s write condition and role-specific tool exposure. It provides an auditable admission boundary, not a proof of verifier soundness. The implementation rejects revoked predecessors before verification and again at insertion, but does not require all predecessor identifiers to resolve or enforce acyclicity. A dependency-closed DAG additionally requires a valid local citation protocol.

If an accepted result is later challenged, revoking u removes its recorded descendants:

A revocation log preserves the decision. This repairs the recorded dependency structure; omitted dependencies remain outside the cascade.

A.3 Annotations, curator contract, staleness, and frontier ranking

An annotation a=(v,z,s,e,c,τ) records a node v, status z, optional score s∈[0,1], evidence identifiers e, rationale c, and timestamp τ. Its current view is

An absent status defaults to open, and an absent score remains unset (⊥). The final appended event wins; timestamps do not select the current annotation, and earlier scores are not averaged.

The curator interprets exploration relations using an AND–OR contract. Let 𝒪⁡(r) be the obligations of an AND route and clt​(v) mean that v is marked closed. Representative rules are

For localization, 𝒪⁡(r) includes reassembly: solving local pieces alone does not close the theorem. A reduction requires an accepted bridge; equivalence requires both directions, and generalization requires a specialization argument. Failed OR branches leave other routes available. These are curator instructions, not a symbolic inference engine. The store validates relation types and score ranges; mathematical witnessing and propagation remain agent responsibilities.

The default frontier 𝒱t contains open or active plans, directions, and annotated symbolic goals. New incident edges identify judgments needing reconsideration:

Missing timestamps and an empty maximum take value −∞. For incident-edge count dtX​(v), define s¯t​(v)=0 if st(v)=⊥ and s¯t​(v)=st​(v) otherwise. The implemented ranking is

Linked nodes precede unlinked nodes, scored nodes precede unscored nodes, and higher scores precede lower scores. Ties favor older entries; symbolic goals use their latest annotation time for ct​(v). The tool exposes a ranked worklist, while the curator supplies its judgments. The contract asks for an exploration bonus and permits strategic guidance to override ranking; no fixed UCB equation or learned scoring model is implemented. Staleness detects newer edges rather than semantic changes to evidence.

A.4 Lexical scoring and neighborhood retrieval

For tokenized corpus 𝒟 of size N, query q, and document d, the implemented BM25 [Robertson and Zaragoza, 2009] score is

Here n⁡(x,⋅) counts occurrences, df⁡(x) counts documents containing x, k1=1.5, and b=0.75. Query multiplicity therefore matters. Tokenization lowercases ASCII letters, digits, and underscores. Empty queries or corpora score zero; an all-empty corpus uses normalization term k1. Fact search indexes stored Markdown and returns positive-scoring identifiers and statements. Agents read proofs separately, and indexes are rebuilt from stored content on demand.

For a selected fact identifier u, fact_neighbors retrieves declared predecessors and nearby exploration facts. With u∼Xv denoting an exploration edge in either direction, the eligible overlay set is

Traversal is undirected; returned paths preserve edge labels and directions for interpretation, without asserting entailment.

Let PB​(u)=firstB⁡(P⁡(u)) preserve the stored predecessor order, and let Hrscan​(u) select the first r distinct overlay facts in edge-log traversal order. The default result sequence is

Here ∥ concatenates sequences, and no overlay results are added when the budget is exhausted. Predecessors receive priority; the overlay cap is applied before predecessor duplicates are removed, so the result can underfill its budget. Optional immediate dependents consume budget between predecessors and overlay facts, and their count is always reported. These operations return statements and connecting paths; they leave proof inspection and local admission to the agent.

A.5 Scope, scoped recall, and lesson continuation

Let 𝒫 denote available projects, β⁡(p) their optional batch labels, and σ the memory mode. Fact statements and negative findings are retrieved from

The gateway defaults to off, including for invalid mode values. Batch membership establishes visibility, not chronology. A sequential evaluation additionally requires 𝒰σ​(pj)⊆{p1,…,pj−1}, and earlier projects must stop changing at their designated boundary. The operator must enforce these conditions through project visibility and termination; recall itself has no completion or timestamp filter.

Recall searches fact statements, negative findings (dead ends, obstacles, and counterexamples), and methodological lessons separately. For requested channels 𝒞 and eligible corpus 𝒟c, it returns

Top+ retains only positive scores. The default budget gives five results to each of three channels; scores are corpus-specific and are not jointly normalized. In batch mode, queryable lessons may come from 𝒰σ​(p)∪{p}; in all mode, the deployment lesson log is unfiltered. Thus a current-project lesson can be recalled even though current-project facts and negative findings are excluded from this tool. Returned facts contain statements rather than proofs, retain their source provenance, and require local reproof and admission under the worker contract. Strategic guidance and progress elaborations are excluded from recall.

At orderly project close, the curator may record ℓ=(pattern,evidence,adjustment): a recurring scoring habit, supporting outcome evidence, and a proposed adjustment. Each text field must satisfy

The store strips validated fields and appends author, source project, and timestamp. The contract limits lessons to methodology; no semantic filter enforces that restriction. For optional retrospective Δ​Λj, the next curator starts with

Launch eligibility selects no lessons in off, sources from the same nonempty batch in batch, and all lessons in all; recency follows append order. Workers and the main agent query lessons, while the curator receives this initial context. Retrospectives are optional and can be lost at abrupt termination, so persistent memory does not by itself imply improvement across tasks.

Appendix B Statements of Partially Solved Open Problems

811.

An edge-colouring of Kn with m=e⁡(G) colours is balanced when n≡1(modm) and every vertex meets every colour equally often. Erdős, Pyber and Tuza asked which graphs G appear as rainbow subgraphs in every large balanced colouring [Erdős and Tuza, 1993; Bloom, 2026h]. Axenovich and Clemen showed that most cliques fail, and conjectured that Kq fails for every q≥4 [Axenovich and Clemen, 2024]. Clemen and Wagner settled q=4 [Clemen and Wagner, 2023]. Ansatz gives a finite balanced base colouring with no rainbow Kq for every q≥4, then lifts it to arbitrarily large admissible orders by the amplification of Axenovich and Clemen [2024]. For q≥12 the base is a pairing of cyclic distances on ℤN with N=4​(q2)+1. The eight bases with q≤11 were checked by exhaustive search. This settles every clique. The question for a general graph, including C6, stays open.

644.

Let f⁡(k,7) be the largest transversal number of a k-uniform family in which every seven members have a two-point transversal. The conjectured order is 34​k [Erdős et al., 1992; Bloom, 2026g]. Fon-Der-Flaass, Kostochka and Woodall proved f⁡(k,7)≤⌈7​k/8⌉ [Fon-Der-Flaass et al., 1999]. For k≥150, Ansatz gives f⁡(k,7)≤⌈(6​k+3)/7⌉+1, hence lim supf⁡(k,7)/k≤6/7.

561.

For star forests F1=⋃iK1,ni and F2=⋃jK1,mj, write L for the sum of the diagonal maxima lk=max⁡{ni+mj−1:i+j=k}. Burr, Erdős, Faudree, Rousseau and Schelp conjectured R^​(F1,F2)=L [Burr et al., 1978; Bloom, 2026f]. The formula was known for uniform forests, for a single star, for two equal stars, and when every size is odd [Davoodi et al., 2025]. Ansatz proves it when one side is two stars of arbitrary sizes and the other side is an arbitrary star forest.

993.

Erdős asked whether the independence sequence ik​(T) of every tree, or forest, is unimodal [Bloom, 2026i]. Basit and Galvin showed the sequence is nondecreasing through roughly n/8 for trees [Basit and Galvin, 2021]. Ansatz produced a proof that every forest increases strictly while through the first 131520​n terms, lifting the increasing prefix from Basit and Galvin’s n/8 to slightly past n/4. For forests of maximum degree at most four it proved strict increase through 0.276​n, which is sharp since the path stops exactly there. The conjecture itself remains open.

1063.

Let nk be the least n≥2​k for which exactly k−1 of n,n−1,…,n−k+1 divide (nk) [Erdős and Selfridge, 1983; Bloom, 2026a]. Monier proved nk≤k! for k≥3, and Cambie improved this to nk≤exp⁡((1+o⁡(1))​k) [Monier, 1985; Bloom, 2026a]. The catalogue discussion also records lower bounds depending on the prime factorization of k [rickyc, 2026]. A later AI-generated report claims nk≤exp⁡(C​k​log⁡log⁡k/log⁡k) for an unspecified constant C [Erdős Problem a Day, 2026]. For sufficiently large k, Ansatz proves

where η>0 is an absolute constant from the Fourier construction. The lower argument combines primes in short intervals with rational approximation; the upper argument constructs admissible integers using nonnegative Fourier coefficients. These bounds give a super-polynomial lower bound and refine the previously claimed upper bound. A matching growth estimate remains open.

302.

Let f⁡(N) be the largest size of a subset of {1,…,N} containing no distinct a,b,c with 1/a=1/b+1/c [Erdős and Graham, 1980; Bloom, 2026c]. The catalogue records Cambie’s asymptotic lower coefficient 5/8 and van Doorn’s upper coefficient 9/10 [Bloom, 2026c]. Khanukov’s preprint gives a non-explicit positive gain over 5/8 and an upper coefficient 140803024/163562355<0.860853 [Khanukov, 2026]. Ansatz proves f⁡(N)=c​N+o⁡(N), characterizes c as an infimum of approximations using finite sets of primes, and gives an explicit convergence rate. It also proves c≥5/8+exp⁡(−100000000030), making the lower gain explicit. The exact value of c remains open.

注意转载授权 · 阅读原文