AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. Extensive efforts on AI4Math have mirrored techniques in NLP, in particular, training large language models on carefully curated math datasets in text form. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. In this position paper, we advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level. In recent years, we have seen steady progress in using AI to perform formal reasoning, including core tasks such as theorem proving and autoformalization, as well as emerging applications such as verifiable generation of code and hardware designs. However, significant challenges remain to be solved for AI to truly master mathematics and achieve broader impact. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success. At this inflection point for formal mathematical reasoning, we call on the research community to come together to drive transformative advancements in this field.

翻译：数学人工智能（AI4Math）不仅在智力层面引人入胜，而且对于科学、工程及其他领域的人工智能驱动发现至关重要。当前对AI4Math的大量研究工作借鉴了自然语言处理的技术，特别是在精心整理的文本形式数学数据集上训练大语言模型。作为一种互补但探索较少的途径，形式化数学推理建立在证明辅助器等形式系统之上，这些系统能够验证推理的正确性并提供自动反馈。在本立场文件中，我们倡导形式化数学推理，并论证其对将AI4Math推向更高水平不可或缺。近年来，我们见证了人工智能在执行形式化推理方面取得的稳步进展，包括定理证明与自动形式化等核心任务，以及可验证的代码与硬件设计生成等新兴应用。然而，要使人工智能真正掌握数学并产生更广泛的影响，仍有重大挑战亟待解决。我们总结了现有进展，讨论了开放挑战，并展望了衡量未来成功的关键里程碑。在形式化数学推理的这一转折点上，我们呼吁研究界携手共进，共同推动该领域的变革性进展。