AI4Math review: from guiding conjectures to formal proofs, AI now solves PKU graduate exams and verifies Erdős counterexamples in Lean

The review argues that AI4Math is not merely applying AI to mathematics but also using mathematics as a premier testbed for general reasoning, and divides the field into two complementary directions: problem-specific modeling and general-purpose modeling. Compared with prior surveys organized by task or model, this offers a unified conceptual framework: problem-specific modeling (guiding intuition, constructing counterexamples, formal reasoning in closed systems) and general-purpose modeling (natural language reasoning, formal reasoning, mathematical information retrieval), clarifying their trade-offs in data, compute, and transferability. This is a conceptual survey and taxonomy, grounded in a synthesis of representative works and the framework diagram in Figure 1, rather than new experimental data.

The authors' PKU evaluation shows reasoning-enhanced models can handle a substantial portion of graduate mathematics: on 11 undergraduate final exams GPT-4 averages 59.6 while o1 scores 89.7, DeepSeek-R1 85.0, o3-mini 92.2, and Gemini 2.5 Pro 94.2; o3-mini averages 84.4 on 58 PhD qualifying exam problems, strongest in Algebra and weakest in Geometry & Topology. Compared with prior results reporting only competition or undergraduate benchmarks, this compares five models across both undergraduate and PhD levels under one human grading rubric (0–5), and reports subject-wise strengths and weaknesses. 100 undergraduate problems from 11 subjects and 58 PhD problems from four fields, graded by human experts on a 0–5 scale; the authors also caution about potential data contamination and the difference between exam problems and open research.

The review notes that formal systems provide verifiable supervision for AI and documents practical results from formal reasoning agents: Aletheia solved 6 of 10 FirstProof problems, Numina-Lean-Agent solved all problems in the 2025 Putnam Competition, and agents such as Aristotle took part in formal verification workflows for Erdős problems (e.g., a counterexample to #205 and partial resolution of #367). Compared with earlier formal-proving work focused on benchmarks, this emphasizes agentic workflows that convert frontier models' heuristic outputs into machine-checkable conclusions in Lean, easing the verification bottleneck in research-level mathematics. Based on specific systems and results cited in the review, including mathlib4 containing over 250,000 theorems and 120,000 definitions as of December 2025 and milestones such as the Liquid Tensor Experiment; the authors describe the Erdős-related cases as representative rather than definitive.

The review distills future directions into seven points, centered on: domain expertise and feature engineering remaining indispensable, the verification bottleneck and autoformalization, semantic consistency in formalization, moving beyond correctness to understanding, from heuristics to expert routines, active community participation, and embracing AI as a research copilot. Compared with discussions focused only on model capability, this centers on 'verification leverage': generating candidate solutions is expensive while verifying them is relatively cheap, so even if AI's reasoning has low correctness probability, overall research efficiency can improve when verification is cheap. This is an argument and outlook grounded in the surveyed progress, citing views from Thurston, Ulam, and Georgiev et al.; it is a position piece rather than an experimental conclusion.

This review is aimed at readers who want a quick overview of AI4Math, including mathematicians, AI researchers, and engineering practitioners. It explicitly limits its scope to mathematical reasoning (discovery, formalization, proof) and does not cover AI for computational mathematics and scientific computing (e.g., PDEs, optimization, inverse problems), referring readers to other surveys. The PKU evaluation applies to the setting of undergraduate and PhD qualifying exams, and the authors caution that exam problems differ from open research and that data contamination is possible. The review's conclusions are suited to understanding current capability boundaries and research directions rather than providing directly applicable engineering recipes.

Readers should keep several points in mind: the PKU evaluation is based on exam problems, the authors themselves caution about potential data contamination, and exam problems differ in nature from open research questions, so the scores should be read as capability signals rather than direct measures of research ability. The Erdős-related formalization results are described by the authors as representative rather than definitive, and while formalization greatly reduces the risk of irreparable hallucinations, it does not eliminate all failure modes—models may still exploit unintended problem specifications or rediscover arguments later found in the literature. In addition, the review only mentions computational mathematics and scientific computing without elaborating, so readers interested in PDEs, optimization, or inverse problems need to look elsewhere.