[Submitted on 8 Jul 2026 (v1), last revised 2 Nov 2026 (this version, v3)]
Authors:Eric Jiang, Xiao Liang, Junyi Zhang, Justin Baker, Zhi Zhang, Yingjia Wan, Yubei Li, Jinxi Yu, Mengting Li, Haikang Deng, Alexander Taylor, Rushil Raghavan, Michael Simon, Hyunsik Chae, Jia-Chen Gu, Xinjie He, Kyle Hess, Ethan Ji, Yiwen Kou, Tzu-Han Lin, Jiachen Lu, Jack Mauro, Vigyan Sahai, Zheng Tan, Alexander Taylor, Junkai Zhang, Kyle Zheng, Lunji Zhu, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang
Abstract:Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.
Submission history
From: Eric Jiang [view email]
[v1] Wed, 8 Jul 2026 17:46:36 UTC (1,544 KB)
[v2] Mon, 19 Oct 2026 16:53:53 UTC (2,981 KB)
[v3] Mon, 2 Nov 2026 19:18:01 UTC (7,892 KB)
