# GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

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

## Key facts

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

## Placed in

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

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

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://mlsanity.com/paper/2409.12122/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [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)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Magicoder: Empowering Code Generation with OSS-Instruct](https://mlsanity.com/paper/2312.02120/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (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)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [A Minimalist Approach to LLM Reasoning: from Rejection Sampling to Reinforce](https://mlsanity.com/paper/2504.11343/) (2025)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [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)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Let's Synthesize Step by Step: Iterative Dataset Synthesis with Large Language Models by Extrapolating Errors from Small Models](https://mlsanity.com/paper/2310.13671/) (2023)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability](https://mlsanity.com/paper/2505.23703/) (2025)
- [FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4](https://mlsanity.com/paper/2503.03238/) (2025)

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

- [Hardening Agent Benchmarks with Adversarial Hacker-Fixer Loops](https://mlsanity.com/paper/2606.08960/) (2026)
- [PhysProver: Advancing Automatic Theorem Proving for Physics](https://mlsanity.com/paper/2601.15737/) (2026)
- [Right in the Right Way: LM Training with Verifiable Rewards and Human Demonstrations](https://mlsanity.com/paper/2607.01181/) (2026)
- [Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory](https://mlsanity.com/paper/2606.06523/) (2026)
- [Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation](https://mlsanity.com/paper/2606.19315/) (2026)
- [Scalable Weak-to-Strong Verifier Hardening for Agent Environments](https://mlsanity.com/paper/2610.15924/) (2026)

## Abstract (arXiv)

Solving math problems through verifiable languages such as Lean has significantly impacted both the mathematics and computer science communities. Current state-of-the-art models are often trained with expensive online Reinforcement Learning (RL) or expert iteration. However, these approaches rely on fixed problem sets, which causes inefficient training and limits the model to tackle complex problems. To overcome these limitations, we propose **GAR**: *Generative Adversarial Reinforcement learning*, a comprehensive RL training framework that jointly trains the problem composer and solver in an adversarial loop. **GAR** introduces an implicit curriculum learning mechanism, which aligns task difficulty with the prover's evolving capability. It thereby improves the training efficiency and enables stronger performance of proving advanced theorems. Experiments show that with **GAR** training, Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B achieve an average relative improvement in pass@32 of **4.20%** on MiniF2F-Test benchmark, while DeepSeek-Prover-V2's pass@32 on ProofNet-Test increases from 22.58% to **25.81%**. Beyond formal proving, **GAR** establishes a general RL paradigm for co-evolution of problem generation and solving under verifiable environments. The training code for this paper is open-sourced in https://github.com/RickySkywalker/GAR-Official