# FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

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

## Key facts

- Cited by 48 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 29 of its 52 references that are in the map.
- First posted on arXiv 5 May 2025.

## Placed in

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

## Builds on (most cited first, 29 of 29)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Qwen Technical Report](https://mlsanity.com/paper/2309.16609/) (2023)
- [Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters](https://mlsanity.com/paper/2408.03314/) (2024)
- [s1: Simple test-time scaling](https://mlsanity.com/paper/2501.19393/) (2025)
- [OpenAI o1 System Card](https://mlsanity.com/paper/2412.16720/) (2024)
- [Kimi k1.5: Scaling Reinforcement Learning with LLMs](https://mlsanity.com/paper/2501.12599/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models](https://mlsanity.com/paper/2410.07985/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [HARDMath: A Benchmark Dataset for Challenging Problems in Applied Mathematics](https://mlsanity.com/paper/2410.09988/) (2024)
- [U-MATH: A University-Level Benchmark for Evaluating Mathematical Skills in LLMs](https://mlsanity.com/paper/2412.03205/) (2024)
- [Verbalized Machine Learning: Revisiting Machine Learning with Language Models](https://mlsanity.com/paper/2406.04344/) (2024)
- [Generating Symbolic World Models via Test-time Scaling of Large Language Models](https://mlsanity.com/paper/2502.04728/) (2025)

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

- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization](https://mlsanity.com/paper/2507.06181/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities](https://mlsanity.com/paper/2505.12680/) (2025)
- [LeanGeo: Formalizing Competitional Geometry problems in Lean](https://mlsanity.com/paper/2508.14644/) (2025)
- [EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty](https://mlsanity.com/paper/2510.00732/) (2025)
- [Autoformalizer with Tool Feedback](https://mlsanity.com/paper/2510.06857/) (2025)
- [LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning](https://mlsanity.com/paper/2603.21065/) (2026)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [StatEval: A Comprehensive Benchmark for Large Language Models in Statistics](https://mlsanity.com/paper/2510.09517/) (2025)
- [TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?](https://mlsanity.com/paper/2603.12744/) (2026)
- [From Chatbot to Digital Colleague: The Paradigm Shift Toward Persistent Autonomous AI](https://mlsanity.com/paper/2606.14502/) (2026)
- [FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory](https://mlsanity.com/paper/2510.02335/) (2025)
- [Why GRPO Needs Normalization: A Local-Curvature Perspective on Adaptive Gradients](https://mlsanity.com/paper/2601.23135/) (2026)
- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning](https://mlsanity.com/paper/2605.28365/) (2026)
- [LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization](https://mlsanity.com/paper/2607.20503/) (2026)
- [GSM-Plus-BN: A Perturbation-Based Benchmark for Bangla Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2607.13248/) (2026)
- [Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs](https://mlsanity.com/paper/2507.04719/) (2025)
- [Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training](https://mlsanity.com/paper/2511.13043/) (2025)

## Abstract (arXiv)

Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning.