FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

TL;DR

The paper introduces FormalMATH, a large-scale Lean4 benchmark (5{,}560 problems) for formal mathematical reasoning and a human-in-the-loop autoformalization pipeline to efficiently translate natural-language problems into Lean4 statements.It provides a comprehensive evaluation of state-of-the-art LLM-based theorem provers, revealing significant challenges including domain bias, overreliance on simple tactics, and limited gains from test-time scaling or reasoning prompts.Key findings show top provers achieving only around $16.46\%$ success on the full benchmark, with CoT-based guidance sometimes reducing performance, highlighting gaps in cross-domain generalization and proof strategy.Overall, FormalMATH offers a robust benchmark and actionable insights to push toward more reliable and domain-robust formal mathematical reasoning in AI systems.

Abstract

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.

Figures (8)

• Figure 1: A human-in-the-loop pipeline for formal mathematical statement creation and filtering.
• Figure 2: (a) Performance comparison of existing theorem provers on the full FormalMATH benchmark. Results show Pass@1$\times$32$\times$100 accuracy for best-first-search-based (BFS) methods, including BFS-Prover and InternLM-Prover, and Pass@32 accuracy via single-pass generations (SPG) for the other provers, including Kinima-Prover, STP, Goedel-Prover, DeepSeek-V1.5-RL and DeepSeek-V1.5-SFT. (b) Funnel chart illustrating the percentage of data that is preserved after each filtering stage in our human-in-the-loop autoformalization pipeline.
• Figure 3: The distribution of mathematical domains in the full set of FormalMATH.
• Figure 4: Our efficient Lean4 verifier implementation.
• Figure 5: Breakdown of accuracy by mathematical domain within FormalMATH.