RMAv2: Context-Orchestrated Research Math Agents

Large language models can produce research-level proofs that are locally convincing yet globally incomplete because they leave a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents v2 (\modelname), an agentic framework that treats proof development as a persistent, issue-driven process. 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 allows \modelname to identify, prioritize, and repair missing proof steps while preserving progress across rounds. Across complementary evaluation settings, \modelname consistently outperforms strong baselines. On the independently evaluated SOOHAK Challenge Hard set, it achieves a 42.5\% solve rate, compared with 12.5\% for its standalone Claude Opus 4.8 backbone. Under blind human-expert evaluation on First Proof, \modelname obtains 8 of 10 correct solutions on B1 and 8 of 10 passing solutions on B2, surpassing GPT-5.2R, Aletheia, ProofCouncil, and other research-math agents at a cost comparable to leading agentic pipelines. \modelname also achieves the strongest results on ResearchMath and Formal Conjectures, with better lemma decomposition and higher Lean~4-verified success on both open and solved research problems.