摘要
近年来，人工智能在数学领域（AI4Math）的发展，尤其是大型语言模型（LLM）驱动的定理证明器，在通过交互式定理证明（ITP）语言生成正式证明方面取得了显著成功。然而，现有系统在应对前沿研究数学方面依然存在根本性限制，例如发现新定理或解决开放猜想，这些问题通常是开放式、欠定义的，并涉及多个抽象层次。
我们认为，AI4Math系统的下一次飞跃需要从预定义的问题求解器转向能够以严格的正式数学推理应对前沿数学挑战的研究代理。在这篇立场论文中，我们系统地回顾了该领域，涵盖了数据集、自动形式化和证明合成。
更重要的是，我们识别了现有系统作为数学研究代理的核心局限性，审视了数据集、关系结构、数学探索、工具生态系统和人机协作等方面的问题，并为AI4Math的未来制定了战略路线图。
博主点评： 这篇论文深入探讨了大型语言模型在数学研究中的应用潜力，指出了现有系统的不足，并为未来的研究提供了清晰的方向。AI4Math的进步不仅依赖于技术的提升，更需要系统性思考与跨学科的合作。