Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and conjectures are often too broad, underspecified, or difficult to connect to plausible proof or refutation strategies.
The paper introduces the AI Mathematician (AIM) framework, which leverages Large Reasoning Models (LRMs) to tackle frontier mathematical research. AIM addresses the complexity and procedural rigor of research problems through an exploration mechanism for longer solution paths and a pessimistic reasonable verification method for reliability. Early experiments show AIM can autonomously construct significant proof components and uncover non‑trivial insights across real‑world mathematical topics.
By Yuanhang Liu, Yanxing Huang, Yanqiao Wang, Peng Li, Yang Liu
EPOCH is an evidence‑governed architecture for AI research agents that improves how candidate discoveries are evaluated and validated. By combining explicit task contracts, typed memory, active falsification, admission checks, and independent replay, EPOCH ensures that each candidate is judged against the strength and scope of its claim. The system achieves state‑of‑the‑art performance on several benchmarks, including AlgoTune, Math14, and AgentHPO, and demonstrates significant advances in executable constructions, algorithm optimization, counterexamples, and proof‑supported results across ten discovery problems.
By Binjie Guo, Aisheng Mo, Ruitong Li, Xinle Deng
The paper introduces Ansatz, a mathematical research agent that uses Continual Graph Memory to organize and reuse intermediate proof results across multiple problems. The system represents facts, plans, and counterexamples in a unified graph, enabling dependency-aware retrieval, evidence-sensitive curation, and scoped recall to guide long-horizon proof searches. Experiments show Ansatz solves all ten First Proof Second Batch problems, tackles the Jamison caterpillar conjecture, and makes progress on several Erdős problems without human help.
By Junyi Zhang, Jinxi Yu, Eric Hanchen Jiang, Jiachen Lu, Zhi Zhang, Xinjie He, Hyunsik Chae, Ethan Ji, Alexander K Taylor, Vigyan Sahai, Yiwen Kou, Kai-Wei Chang, Raghu Meka, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang
The paper introduces SCOPE, a framework that enables multiple scientist agents to pursue conjecture-driven research trajectories by modeling equations, formulating questions, and conducting active experiments, then sharing evidence to refine their conjectures. It also presents ClosureBench, an interactive benchmark of 60 closure-discovery tasks across five scientific domains, designed to evaluate equation discovery beyond accuracy by measuring evidence faithfulness, mechanism insight, and experimental effectiveness. Experiments show that SCOPE outperforms diverse baselines on both ClosureBench and a real-world scientific discovery case, yielding more accurate, reliable, and effective scientific discoveries.
By Yuxiao Hu, Qian Li, Ding Wang, Siheng Chen, Linfeng Zhang, Jinyue Yan, Yuntian Chen
Cogentic is a multi‑agent system designed to automate proof discovery for open research problems. It uses an iterative prove‑verify loop where an orchestrator assigns independent provers to different proof directions, verifies their outputs with specialized components, and records confirmed intermediate results in a persistent ledger for future rounds. Built on Gemini, Cogentic has produced novel results on five open problems in online learning, auction theory, and mechanism design, each verified by domain experts and detailed in companion papers.
By Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang