# RMA: an Agentic System for Research-Level Mathematical Problems

arXiv: https://arxiv.org/abs/2605.22875 · HTML: https://mlsanity.com/paper/2605.22875/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 32 of its 48 references that are in the map.
- First posted on arXiv 20 May 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 30 of 32)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [MemGPT: Towards LLMs as Operating Systems](https://mlsanity.com/paper/2310.08560/) (2023)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [AFlow: Automating Agentic Workflow Generation](https://mlsanity.com/paper/2410.10762/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [ReasoningBank: Scaling Agent Self-Evolving with Reasoning Memory](https://mlsanity.com/paper/2509.25140/) (2025)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Agentic Reasoning: A Streamlined Framework for Enhancing LLM Reasoning with Agentic Tools](https://mlsanity.com/paper/2502.04644/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Evaluating Mathematical Reasoning of Large Language Models: A Focus on Error Identification and Correction](https://mlsanity.com/paper/2406.00755/) (2024)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)
- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [First Proof](https://mlsanity.com/paper/2602.05192/) (2026)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [Exploring Advanced LLM Multi-Agent Systems Based on Blackboard Architecture](https://mlsanity.com/paper/2507.01701/) (2025)
- [AI for Auto-Research: Roadmap & User Guide](https://mlsanity.com/paper/2605.18661/) (2026)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models](https://mlsanity.com/paper/2602.16793/) (2026)
- [Aletheia tackles FirstProof autonomously](https://mlsanity.com/paper/2602.21201/) (2026)
- [Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving](https://mlsanity.com/paper/2505.20869/) (2025)

## Built on by (most cited first, 7 of 7)

- [ProofCouncil: An LLM Agent for Solving Open Mathematical Problems](https://mlsanity.com/paper/2607.09474/) (2026)
- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026)
- [WorldBagel: Uncovering the Power of Unified Multimodal Models for Vision-Language-Action-World Modeling](https://mlsanity.com/paper/2607.03461/) (2026)
- [Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research](https://mlsanity.com/paper/2608.15052/) (2026)
- [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)

## Abstract (arXiv)

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.