# DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

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

## Key facts

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

## Placed in

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

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

- [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)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [OpenAI o1 System Card](https://mlsanity.com/paper/2412.16720/) (2024)
- [Open-Reasoner-Zero: An Open Source Approach to Scaling Up Reinforcement Learning on the Base Model](https://mlsanity.com/paper/2503.24290/) (2025)
- [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)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [CMATH: Can Your Language Model Pass Chinese Elementary School Math Test?](https://mlsanity.com/paper/2306.16636/) (2023)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [MathOdyssey: Benchmarking Mathematical Problem-Solving Skills in Large Language Models Using Odyssey Math Data](https://mlsanity.com/paper/2406.18321/) (2024)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation](https://mlsanity.com/paper/2505.10962/) (2025)

## Built on by (most cited first, 24 of 24)

- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [RLVER: Reinforcement Learning with Verifiable Emotion Rewards for Empathetic Agents](https://mlsanity.com/paper/2507.03112/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models](https://mlsanity.com/paper/2506.17114/) (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)
- [KaVa: Latent Reasoning via Compressed KV-Cache Distillation](https://mlsanity.com/paper/2510.02312/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [Masked-and-Reordered Self-Supervision for Reinforcement Learning from Verifiable Rewards](https://mlsanity.com/paper/2511.17473/) (2025)
- [Milestones over Outcome: Unlocking Geometric Reasoning with Sub-Goal Verifiable Reward](https://mlsanity.com/paper/2601.05073/) (2026)
- [Evaluation of LLMs for Mathematical Formalization in Lean](https://mlsanity.com/paper/2606.05632/) (2026)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)
- [Learning to Reason with Insight for Informal Theorem Proving](https://mlsanity.com/paper/2604.16278/) (2026)
- [Mathematics with large language models as provers and verifiers](https://mlsanity.com/paper/2510.12829/) (2025)
- [Monotonic Reference-Free Refinement for Autoformalization](https://mlsanity.com/paper/2601.23166/) (2026)
- [Pipeline for Verifying LLM-Generated Mathematical Solutions](https://mlsanity.com/paper/2602.20770/) (2026)
- [OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving](https://mlsanity.com/paper/2604.23712/) (2026)
- [Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery](https://mlsanity.com/paper/2606.08728/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Reliable Use of Lemmas via Eligibility Reasoning and Section-Aware Reinforcement Learning](https://mlsanity.com/paper/2602.00998/) (2026)
- [AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification](https://mlsanity.com/paper/2607.11849/) (2026)
- [MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement](https://mlsanity.com/paper/2608.14221/) (2026)
- [SAGE: Mitigating Long-Horizon Reasoning Biases via Topological Guidance](https://mlsanity.com/paper/2609.30192/) (2026)
- [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026)

## Abstract (arXiv)

Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.