Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery

• URL: http://arxiv.org/abs/2606.08728v1
• Date: Sun, 07 Jun 2026 16:50:07 GMT
• Title: Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery
• Abstract summary: This survey provides a unified account of the field's evolution.<n>We organize the landscape along four axes: (i) informal reasoning over text and diagrams, spanning MWP solving, multimodal geometry, and RLMs; (ii) formal reasoning in proof assistants, including autoformalization, tactic prediction, compiler-guided repair, and proof search; (iii) mathematical discovery, where systems propose constructions, improve bounds, or assist attacks on open problems; and (iv) the inference and training-time techniques, including CoT prompting, tool use, process reward models, and VLVR, that increasingly connect generation with
• Score: 3.9943798586374784
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Mathematical reasoning has long served as a stringent test of machine intelligence; over the past decade, it has moved from a niche problem within NLP to one of the most consequential AI frontiers. This survey provides a unified account of the field's evolution, from early rule-based math word problem (MWP) solvers and template-driven geometry systems, through neural expression generation and LLM prompting, to contemporary reasoning models, multi-agent systems, neuro-symbolic theorem provers, and verified discovery workflows. We organize the landscape along four axes: (i) informal reasoning over text and diagrams, spanning MWP solving, multimodal geometry, and VLMs; (ii) formal reasoning in proof assistants, including autoformalization, tactic prediction, compiler-guided repair, and proof search; (iii) mathematical discovery, where systems propose constructions, improve bounds, or assist attacks on open problems; and (iv) the inference and training-time techniques, including CoT prompting, tool use, process reward models, and RLVR, that increasingly connect generation with verification. We catalog major benchmarks across grade-school arithmetic, competition mathematics, geometry, formal proving, multimodal and multilingual reasoning, and expert evaluation, and we examine benchmark saturation, contamination, reporting mismatches, and the distinction between pass@1, majority voting, and verifier-assisted pass@$k$. We critically assess failure modes: brittleness under perturbation, reward hacking, multimodal grounding failures, fragile formalization, and the energy cost of reasoning-scale inference. Drawing on recent perspectives from working mathematicians, we identify future directions centered on verified-discovery workflows, reasoning efficiency, and infrastructure to make AI-assisted formalization broadly usable. Companion materials: https://github.com/Starscream-11813/awesome-AI4Math.

Related papers

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• MechMath Agent Team: LLM Driven Agents for Mathematical Research [17.23955320294417]
  MechMath Agent Team (MMAT) is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research.<n>We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes.<n>We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities.
  arXiv  Detail & Related papers  (2026-07-05T16:37:40Z)
• Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics [9.38309744591661]
  We present Formal Conjectures, an evolving benchmark of 2615 mathematical problem statements formalized in Lean 4.<n>The dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery.<n>We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community.
  arXiv  Detail & Related papers  (2026-05-13T08:33:15Z)
• Automated Conjecture Resolution with Formal Verification [21.763678203045973]
  We propose an automated framework for tackling research-level mathematical problems.<n>Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon.<n>Using this framework, we automatically resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement.
  arXiv  Detail & Related papers  (2026-04-04T16:35:16Z)
• Deconstructing Multimodal Mathematical Reasoning: Towards a Unified Perception-Alignment-Reasoning Paradigm [82.57296908195654]
  Multimodal Mathematical Reasoning (MMR) has attracted increasing attention for its capability to solve mathematical problems that involve both textual and visual modalities.<n>Current models still face significant challenges in real-world visual math tasks.
  arXiv  Detail & Related papers  (2026-03-09T12:11:00Z)
• Systematic Diagnosis of Brittle Reasoning in Large Language Models [1.14219428942199]
  A central question in artificial intelligence is the extent to which machine learning models comprehend mathematics.<n>We propose a novel framework for measuring mathematical reasoning that moves beyond standard benchmarks to diagnose specific failure points.
  arXiv  Detail & Related papers  (2025-10-05T21:40:09Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  We advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level.<n>We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
  arXiv  Detail & Related papers  (2024-12-20T17:19:24Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  This work investigates the applicability of large language models (LLMs) in formalizing advanced mathematical concepts. We envision an automated process, called emphmath-PVS, to extract and formalize mathematical theorems from research papers.
  arXiv  Detail & Related papers  (2023-10-25T23:54:04Z)
• Large Language Models as Analogical Reasoners [155.9617224350088]
  Chain-of-thought (CoT) prompting for language models demonstrates impressive performance across reasoning tasks. We introduce a new prompting approach, analogical prompting, designed to automatically guide the reasoning process of large language models.
  arXiv  Detail & Related papers  (2023-10-03T00:57:26Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  We review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade. Recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning.
  arXiv  Detail & Related papers  (2022-12-20T18:46:16Z)
• Machine Number Sense: A Dataset of Visual Arithmetic Problems for Abstract and Relational Reasoning [95.18337034090648]
  We propose a dataset, Machine Number Sense (MNS), consisting of visual arithmetic problems automatically generated using a grammar model--And-Or Graph (AOG) These visual arithmetic problems are in the form of geometric figures. We benchmark the MNS dataset using four predominant neural network models as baselines in this visual reasoning task.
  arXiv  Detail & Related papers  (2020-04-25T17:14:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.