From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

从求解器到研究：大语言模型驱动的前沿形式化数学

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. 摘要： 近年来，人工智能数学（AI4Math）领域取得了显著进展，特别是大语言模型（LLM）驱动的定理证明器，通过交互式定理证明（ITP）语言，在解决定义明确的数学问题的形式化证明生成方面取得了巨大成功。

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. 我们认为，AI4Math 系统的下一次飞跃需要实现决定性的转变：从预定义的“问题求解器”转向能够通过严谨的形式化数学推理来应对前沿数学挑战的“研究智能体”。

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. 更重要的是，我们指出了现有系统作为数学研究智能体时的核心局限性，深入探讨了数据集、关系结构、数学探索、工具生态系统以及人机协作等方面的问题，并为 AI4Math 的未来规划了战略路线图。