# Reinforcement Learning of Theorem Proving

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

## Key facts

- Cited by 69 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 May 2018.

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

- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [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)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [Contrastive Reinforcement Learning of Symbolic Reasoning Domains](https://mlsanity.com/paper/2106.09146/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Simplifying Polylogarithms with Machine Learning](https://mlsanity.com/paper/2206.04115/) (2022)
- [Peano: Learning Formal Mathematical Reasoning](https://mlsanity.com/paper/2211.15864/) (2022)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Integration of knowledge and data in machine learning](https://mlsanity.com/paper/2202.10337/) (2022)
- [Towards Tractable Mathematical Reasoning: Challenges, Strategies, and Opportunities for Solving Math Word Problems](https://mlsanity.com/paper/2111.05364/) (2021)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Learning Equational Theorem Proving](https://mlsanity.com/paper/2102.05547/) (2021)
- [Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis](https://mlsanity.com/paper/2205.14229/) (2022)
- [LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions](https://mlsanity.com/paper/2211.08671/) (2022)

## Abstract (arXiv)

We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.