Position: Formal Mathematical Reasoning—A New Frontier in AI

AI for Mathematics (AI4Math) is intellectually intriguing and is crucial for AI-driven system design and verification. 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. This position paper advocates formal mathematical reasoning as an indispensable component in future AI for math, formal verification, and verifiable generation. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.

Many breakthroughs in artificial intelligence (AI) have come from teaching computers to solve math problems written in everyday language. But as math gets more advanced, this informal approach runs into roadblocks —there’s not enough good data to train on, and it’s hard to check if the answers are truly correct.Our paper makes the case for a more rigorous path: using formal mathematical systems—the kind that mathematicians and software engineers use to write precise, verifiable proofs. These systems can act like automatic proof checkers and give helpful feedback when something is wrong. We explore how combining these systems with modern AI models opens up new possibilities, from solving high-level math problems to ensuring the correctness of critical software and hardware systems. We outline the recent progress, challenges ahead, and what success could look like in the coming years.Formal reasoning might sound technical, but it could be key to building trustworthy AI that can reason reliably—in math, in code, and in the world.