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

近期人工智能在数学领域（AI4Math）取得显著进展，特别是基于大语言模型的定理证明器，能通过交互式定理证明语言生成定义明确问题的形式化证明。然而，现有系统在应对发现新定理或解决开放猜想等前沿研究时仍受局限，因这些问题往往开放、未充分指定且涉及多层抽象。本文主张 AI4Math 需从预定义问题求解器转向具备严谨形式化推理能力的研究智能体。文章系统回顾了数据集、自动形式化及证明合成现状，深入剖析了现有系统在作为数学研究智能体时的核心局限，涵盖数据结构、探索机制、工具生态及人机协作等方面，并提出了未来发展的战略路线图。