# Formal Mathematical Reasoning: A New Frontier in AI

arXiv: https://arxiv.org/abs/2412.16075 · HTML: https://mlsanity.com/paper/2412.16075/

## 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.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 30 of 170)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Mamba: Linear-Time Sequence Modeling with Selective State Spaces](https://mlsanity.com/paper/2312.00752/) (2023)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [HotpotQA: A Dataset for Diverse, Explainable Multi-hop Question Answering](https://mlsanity.com/paper/1809.09600/) (2018)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Training Compute-Optimal Large Language Models](https://mlsanity.com/paper/2203.15556/) (2022)
- [Empirical Evaluation of Gated Recurrent Neural Networks on Sequence Modeling](https://mlsanity.com/paper/1412.3555/) (2014)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters](https://mlsanity.com/paper/2408.03314/) (2024)
- [Language Models as Knowledge Bases?](https://mlsanity.com/paper/1909.01066/) (2019)
- [CommonsenseQA: A Question Answering Challenge Targeting Commonsense Knowledge](https://mlsanity.com/paper/1811.00937/) (2018)
- [Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Them](https://mlsanity.com/paper/2210.09261/) (2022)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Large Language Models Can Be Easily Distracted by Irrelevant Context](https://mlsanity.com/paper/2302.00093/) (2023)
- [RWKV: Reinventing RNNs for the Transformer Era](https://mlsanity.com/paper/2305.13048/) (2023)

## Built on by (most cited first, 30 of 81)

- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models](https://mlsanity.com/paper/2503.09567/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [The Landscape of Agentic Reinforcement Learning for LLMs: A Survey](https://mlsanity.com/paper/2509.02547/) (2025)
- [A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systems](https://mlsanity.com/paper/2504.09037/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening](https://mlsanity.com/paper/2506.02355/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [A Survey of Agentic Reasoning for Large Language Models: Towards Recursively Self-Improving and Collective Agents](https://mlsanity.com/paper/2601.12538/) (2026)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [The Attack and Defense Landscape of Agentic AI: A Comprehensive Survey](https://mlsanity.com/paper/2603.11088/) (2026)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [Premise-Augmented Reasoning Chains Improve Error Identification in Math reasoning with LLMs](https://mlsanity.com/paper/2502.02362/) (2025)
- [Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills](https://mlsanity.com/paper/2512.16301/) (2025)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Mathesis: Towards Formal Theorem Proving from Natural Languages](https://mlsanity.com/paper/2506.07047/) (2025)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://mlsanity.com/paper/2506.04592/) (2025)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization](https://mlsanity.com/paper/2507.06181/) (2025)
- [Generative AI Act II: Test Time Scaling Drives Cognition Engineering](https://mlsanity.com/paper/2504.13828/) (2025)
- [(Im)possibility of Automated Hallucination Detection in Large Language Models](https://mlsanity.com/paper/2504.17004/) (2025)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)

## 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.