mlsanityData to 7 Oct 2026

Reinforcement Learning of Theorem Proving

arXiv 1805.07563 ↗First posted 19 May 2018cs.AI cs.LG cs.LOcited by 69

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 16; 2022: 14; 2023: 7; 2024: 13; 2025: 12; 2026: 7.

69 papers.

Sort:

By area:

  1. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  3. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  5. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  6. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  7. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  8. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  9. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  10. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  11. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  12. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
38 more
  1. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  2. 2021Contrastive Reinforcement Learning of Symbolic Reasoning Domainscited by 17
  3. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  4. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  5. 2022Simplifying Polylogarithms with Machine Learningcited by 14
  6. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  7. 2022Integration of knowledge and data in machine learningcited by 13
  8. 2021Towards Tractable Mathematical Reasoning: Challenges, Strategies, and Opportunities for Solving Math Word Problemscited by 12
  9. 2023Alien Codingcited by 9
  10. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  11. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  12. 2022The Isabelle ENIGMAcited by 8
  13. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
  14. 2021Learning Theorem Proving Componentscited by 7
  15. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
  16. 2021Learning Equational Theorem Provingcited by 5
  17. 2022Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesiscited by 5
  18. 2022LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractionscited by 5
  19. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  20. 2021Similarity-Based Equational Inference in Physicscited by 4
  21. 2022Challenges to Solving Combinatorially Hard Long-Horizon Deep RL Taskscited by 4
  22. 2023An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representationscited by 4
  23. 2024Symbolic Equation Solving via Reinforcement Learningcited by 4
  24. 2024Satisficing Exploration for Deep Reinforcement Learningcited by 4
  25. 2025Study and improvement of search algorithms in two-players perfect information gamescited by 4
  26. 2021Graph Contrastive Pre-training for Effective Theorem Reasoningcited by 3
  27. 2022Machine Learning Meets The Herbrand Universecited by 3
  28. 2023Lemmas: Generation, Selection, Applicationcited by 3
  29. 2023Reinforcement Learning and Data-Generation for Syntax-Guided Synthesiscited by 3
  30. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  31. 2025Learning Conjecturing from Scratchcited by 3
  32. 2021A* Search Without Expansions: Learning Heuristic Functions with Deep Q-Networkscited by 2
  33. 2024When Do Skills Help Reinforcement Learning? A Theoretical Analysis of Temporal Abstractionscited by 2
  34. 2025Tandem Training for Language Modelscited by 2
  35. 2022Adversarial Learning to Reason in an Arbitrary Logiccited by 1
  36. 2022Learning to Prove Trigonometric Identitiescited by 1
  37. 2022Project proposal: A modular reinforcement learning based automated theorem provercited by 1
  38. 2023Learning to solve arithmetic problems with a virtual abacuscited by 1

50 most cited of 69 All 69 (JSON)