mlsanityData to 7 Oct 2026

GamePad: A Learning Environment for Theorem Proving

arXiv 1806.00608 ↗First posted 2 Jun 2018cs.LG cs.AI cs.LOcited by 48

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 7; 2022: 6; 2023: 5; 2024: 18; 2025: 8; 2026: 4.

48 papers.

Sort:

By area:

  1. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  5. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  6. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  7. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  10. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  11. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  12. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
36 more
  1. 2024Process-Driven Autoformalization in Lean 4cited by 45
  2. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  3. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  4. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  5. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  6. 2023Mathematical Language Models: A Surveycited by 24
  7. 2025Frontier AI's Impact on the Cybersecurity Landscapecited by 21
  8. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  9. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  10. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  11. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  12. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 9
  13. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  14. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  15. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
  16. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  17. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  18. 2022Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesiscited by 5
  19. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  20. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  21. 2022Gym-saturation: an OpenAI Gym environment for saturation proverscited by 3
  22. 2024NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesiscited by 3
  23. 2024Learning Structure-Aware Representations of Dependent Typescited by 2
  24. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  25. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  26. 2024The Tactician's Web of Large-Scale Formal Knowledgecited by 1
  27. 2024AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofscited by 1
  28. 2025Hierarchical Attention Generates Better Proofscited by 1
  29. 2025Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspectivecited by 1
  30. 2026TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematicscited by 1
  31. 2022Genetic Algorithm for Program Synthesiscited by 0
  32. 2024EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languagescited by 0
  33. 2024Incorporating Graph Attention Mechanism into Geometric Problem Solving Based on Deep Reinforcement Learningcited by 0
  34. 2025Automated Proof of Polynomial Inequalities via Reinforcement Learningcited by 0
  35. 2026Geometric Measurements of the Axiom of Choice in Neural Proof Embeddingscited by 0
  36. 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verificationcited by 0