Position: Formal Mathematical Reasoning—A New Frontier in AI
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri, Dawn Song
Abstract
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.
BibTeX
@inproceedings{
yang2025position,
title={Position: Formal Mathematical Reasoning{\textemdash}A New Frontier in {AI}},
author={Kaiyu Yang and Gabriel Poesia and Jingxuan He and Wenda Li and Kristin E. Lauter and Swarat Chaudhuri and Dawn Song},
booktitle={Forty-second International Conference on Machine Learning Position Paper Track},
year={2025},
url={https://openreview.net/forum?id=HuvAM5x2xG}
}