AI for Mathematics: Progress, Challenges, and Prospects

TL;DR

This paper surveys AI4Math's dual pathways—problem-specific modeling and general-purpose modeling—highlighting how ML accelerates conjecture generation, construction of examples, and formal reasoning within geometry and algebra. It reviews foundation models, neuro-symbolic systems, autoformalization, and agentic theorem proving, illustrating progress from undergraduate to some graduate-level mathematics while identifying remaining gaps toward true research-level expertise. The work emphasizes formal verification as a critical training signal, the need for scalable autoformalization and robust evaluation, and the design of agentic workflows that mimic professional mathematicians. Collectively, the findings argue for close collaboration between AI researchers and mathematicians to build robust, verifiable AI copilots that extend mathematical discovery and understanding beyond mere correctness. The practical impact lies in enabling scalable conjecture testing, rigorous formalization, and automated knowledge retrieval to accelerate mathematical progress across subfields.

Abstract

AI for Mathematics (AI4Math) has emerged as a distinct field that leverages machine learning to navigate mathematical landscapes historically intractable for early symbolic systems. While mid-20th-century symbolic approaches successfully automated formal logic, they faced severe scalability limitations due to the combinatorial explosion of the search space. The recent integration of data-driven approaches has revitalized this pursuit. In this review, we provide a systematic overview of AI4Math, highlighting its primary focus on developing AI models to support mathematical research. Crucially, we emphasize that this is not merely the application of AI to mathematical activities; it also encompasses the development of stronger AI systems where the rigorous nature of mathematics serves as a premier testbed for advancing general reasoning capabilities. We categorize existing research into two complementary directions: problem-specific modeling, involving the design of specialized architectures for distinct mathematical tasks, and general-purpose modeling, focusing on foundation models capable of broader reasoning, retrieval, and exploratory workflows. We conclude by discussing key challenges and prospects, advocating for AI systems that go beyond facilitating formal correctness to enabling the discovery of meaningful results and unified theories, recognizing that the true value of a proof lies in the insights and tools it offers to the broader mathematical landscape.

Figures (2)

• Figure 1: Performance of five LLMs across different Peking University (PKU) exams. Left: Scores on 11 undergraduate subjects. Middle: Average scores of the five LLMs across these subjects. Right: o3-mini’s performance on four PhD qualifying exam fields (average score: 84.4).
• Figure 2: Example of a proof step generation method and the complete proof it produces. Left: An illustration of a proof tree, where each node represents a proof state and each edge corresponds to a tactic. Applying an appropriate tactic transforms the current proof state into the next one. At each step, the proof step generation method retrieves relevant premises and proposes several candidate tactics to try. Right: The complete proof ultimately obtained by this process.