Formal Mathematical Reasoning: A New Frontier in AI

Understand

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.