# GamePad: A Learning Environment for Theorem Proving

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

## Key facts

- Cited by 48 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Jun 2018.

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

- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover](https://mlsanity.com/paper/2407.17227/) (2024)
- [Mathematical Language Models: A Survey](https://mlsanity.com/paper/2312.07622/) (2023)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [Peano: Learning Formal Mathematical Reasoning](https://mlsanity.com/paper/2211.15864/) (2022)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [A Survey on Mathematical Reasoning and Optimization with Large Language Models](https://mlsanity.com/paper/2503.17726/) (2025)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [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)

## Abstract (arXiv)

In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner. Hence, they provide an opportunity to explore theorem proving with human supervision. We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem. We address position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step) tasks, which arise naturally in tactic-based theorem proving.