Position: Formal Mathematical Reasoning—A New Frontier in AI
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.
Cite
Text
Yang et al. "Position: Formal Mathematical Reasoning—A New Frontier in AI." Proceedings of the 42nd International Conference on Machine Learning, 2025.Markdown
[Yang et al. "Position: Formal Mathematical Reasoning—A New Frontier in AI." Proceedings of the 42nd International Conference on Machine Learning, 2025.](https://mlanthology.org/icml/2025/yang2025icml-position-a/)BibTeX
@inproceedings{yang2025icml-position-a,
title = {{Position: Formal Mathematical Reasoning—A New Frontier in AI}},
author = {Yang, Kaiyu and Poesia, Gabriel and He, Jingxuan and Li, Wenda and Lauter, Kristin E. and Chaudhuri, Swarat and Song, Dawn},
booktitle = {Proceedings of the 42nd International Conference on Machine Learning},
year = {2025},
pages = {82384-82398},
volume = {267},
url = {https://mlanthology.org/icml/2025/yang2025icml-position-a/}
}