# TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

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

## Key facts

- Cited by 37 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 63 references that are in the map.
- First posted on arXiv 19 Feb 2021.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [End-to-End Differentiable Proving](https://mlsanity.com/paper/1705.11040/) (2017)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Memory Augmented Policy Optimization for Program Synthesis and Semantic Parsing](https://mlsanity.com/paper/1807.02322/) (2018)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [Natural-Parameter Networks: A Class of Probabilistic Neural Networks](https://mlsanity.com/paper/1611.00448/) (2016)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning](https://mlsanity.com/paper/1807.08058/) (2018)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Towards Finding Longer Proofs](https://mlsanity.com/paper/1905.13100/) (2019)
- [Tactic Learning and Proving for the Coq Proof Assistant](https://mlsanity.com/paper/2003.09140/) (2020)
- [Premise Selection and External Provers for HOL4](https://mlsanity.com/paper/1509.03534/) (2015)
- [Prolog Technology Reinforcement Learning Prover](https://mlsanity.com/paper/2004.06997/) (2020)
- [A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving](https://mlsanity.com/paper/1911.02065/) (2019)

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (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)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [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)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [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)
- [Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving](https://mlsanity.com/paper/2404.07382/) (2024)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Learning the Simplicity of Scattering Amplitudes](https://mlsanity.com/paper/2408.04720/) (2024)
- [3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes](https://mlsanity.com/paper/2410.11133/) (2024)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (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)
- [CoProver: A Recommender System for Proof Construction](https://mlsanity.com/paper/2304.10486/) (2023)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method](https://mlsanity.com/paper/2312.14188/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Learning to Prove Trigonometric Identities](https://mlsanity.com/paper/2207.06679/) (2022)
- [Project proposal: A modular reinforcement learning based automated theorem prover](https://mlsanity.com/paper/2209.02562/) (2022)
- [Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques](https://mlsanity.com/paper/2502.03321/) (2025)

## Abstract (arXiv)

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart from promising alternatives. We implement the framework in the HOL4 theorem prover. Experimental results show that the framework outperforms existing automated theorem provers (i.e., hammers) available in HOL4 when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.