Data to 14 Oct 2026

Formal Mathematical Reasoning: A New Frontier in AI

arXiv 2412.16075 ↗First posted 20 Dec 2024cs.AI cs.LG cs.LOcited by 81

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. 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. In this position paper, we advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level. In recent years, we have seen steady progress in using AI to perform formal reasoning, including core tasks such as theorem proving and autoformalization, as well as emerging applications such as verifiable generation of code and hardware designs. However, significant challenges remain to be solved for AI to truly master mathematics and achieve broader impact. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success. At this inflection point for formal mathematical reasoning, we call on the research community to come together to drive transformative advancements in this field.

Key facts. Cited by 81 papers in the map (data through 14 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 170 of its 277 references that are in the map. First posted on arXiv 20 Dec 2024.

Builds on

170 of 277 references.

Closest ancestors · 21

Same direction, newest first

9 more

Other references · 149

2017Attention Is All You Needcited by 60,361
2023GPT-4 Technical Reportcited by 18,396
2024The Llama 3 Herd of Modelscited by 14,715
2023LLaMA: Open and Efficient Foundation Language Modelscited by 14,132
2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
2021Training Verifiers to Solve Math Word Problemscited by 10,109
2021Evaluating Large Language Models Trained on Codecited by 8,320
2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,708
2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
2023Mamba: Linear-Time Sequence Modeling with Selective State Spacescited by 4,718
2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,182
2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,824

38 more

2023Let's Verify Step by Stepcited by 3,789
2018HotpotQA: A Dataset for Diverse, Explainable Multi-hop Question Answeringcited by 3,754
2021Program Synthesis with Large Language Modelscited by 3,637
2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,373
2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,211
2022Training Compute-Optimal Large Language Modelscited by 3,019
2014Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modelingcited by 2,367
2023Code Llama: Open Foundation Models for Codecited by 2,139
2024Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameterscited by 1,986
2019Language Models as Knowledge Bases?cited by 1,936
2018CommonsenseQA: A Question Answering Challenge Targeting Commonsense Knowledgecited by 1,822
2022Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Themcited by 1,807
2024DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligencecited by 1,181
2023Large Language Models Cannot Self-Correct Reasoning Yetcited by 1,017
2023Large Language Models Can Be Easily Distracted by Irrelevant Contextcited by 841
2023RWKV: Reinventing RNNs for the Transformer Eracited by 827
2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 783
2023MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Modelscited by 735
2023Measuring Faithfulness in Chain-of-Thought Reasoningcited by 703
2022PAL: Program-aided Language Modelscited by 652
2017Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problemscited by 650
2023MAmmoTH: Building Math Generalist Models through Hybrid Instruction Tuningcited by 487
2021Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributionscited by 431
2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
2024TravelPlanner: A Benchmark for Real-World Planning with Language Agentscited by 392
2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 391
2022PlanBench: An Extensible Benchmark for Evaluating Large Language Models on Planning and Reasoning about Changecited by 382
2017Physics Informed Deep Learning (Part I): Data-driven Solutions of Nonlinear Partial Differential Equationscited by 373
2023RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generationcited by 367
2024ReST-MCTS*: LLM Self-Training via Process Reward Guided Tree Searchcited by 344
2023On the Planning Abilities of Large Language Models : A Critical Investigationcited by 312
2022Large Language Models are Better Reasoners with Self-Verificationcited by 307
2024ProcessBench: Identifying Process Errors in Mathematical Reasoningcited by 292
2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
2024Inference Scaling Laws: An Empirical Analysis of Compute-Optimal Inference for Problem-Solving with Language Modelscited by 290
2017Unsupervised Machine Translation Using Monolingual Corpora Onlycited by 273
2023Physics of Language Models: Part 3.1, Knowledge Storage and Extractioncited by 270

50 most cited of 149 All 149 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 56; 2026: 25.

81 papers.

Sort:

By area:

2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 867
2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 384
2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 205
2025A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systemscited by 111
2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 80
2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
2026A Survey of Agentic Reasoning for Large Language Models: Towards Recursively Self-Improving and Collective Agentscited by 50
2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 48
2025VERINA: Benchmarking Verifiable Code Generationcited by 34

38 more

2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 29
2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 28
2026The Attack and Defense Landscape of Agentic AI: A Comprehensive Surveycited by 28
2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
2025Premise-Augmented Reasoning Chains Improve Error Identification in Math reasoning with LLMscited by 22
2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 22
2025Frontier AI's Impact on the Cybersecurity Landscapecited by 21
2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
2026Large Language Model Reasoning Failurescited by 21
2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 18
2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 18
2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 17
2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 16
2025Generative AI Act II: Test Time Scaling Drives Cognition Engineeringcited by 15
2025(Im)possibility of Automated Hallucination Detection in Large Language Modelscited by 15
2025Theorem Prover as a Judge for Synthetic Data Generationcited by 14
2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 14
2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 11
2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 10
2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
2025ReasonBENCH: Benchmarking the (In)Stability of LLM Reasoningcited by 9
2025Mimicking or Reasoning: Rethinking Multi-Modal In-Context Learning in Vision-Language Modelscited by 8
2025EvoCut: Strengthening Integer Programs via Evolution-Guided Language Modelscited by 8
2025Evaluation of LLMs for mathematical problem solvingcited by 7
2025Towards a Common Framework for Autoformalizationcited by 7
2025Autoformalizer with Tool Feedbackcited by 7
2025Knowledge Augmented Complex Problem Solving with Large Language Models: A Surveycited by 6
2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoningcited by 6
2025GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Provingcited by 6
2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 5
2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 5
2025Assessing the Sensitivity and Alignment of FOL Closeness Metricscited by 4
2025LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 4
2025FMC: Formalization of Natural Language Mathematical Competition Problemscited by 4
2026Theory-Scale Auto-Formalization of Logics for Computer Sciencecited by 4

50 most cited of 81 All 81 (JSON)

Similar, not cited

Close in wording, no citation either way