Answers.Body: <p>It is feasible, even though we are at the level of high-school mathematics at the moment. But there is room for scaling. Examples are:</p>
  <p><a href="https://arxiv.org/abs/2205.11491" rel="nofollow noreferrer">HyperTree Proof Search for Neural Theorem Proving (2022)</a></p>
  <p><a href="https://www.arxiv.org/pdf/2408.08152" rel="nofollow noreferrer">DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback
  for Reinforcement Learning and Monte-Carlo Tree Search (2024)</a></p>
  <p>The first paper use a generalization of AlphaZero, while the second build a much more complex pipeline including supervised training, MCTS and reinforcement learning.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2024-09-06T10:34:45.520Z
Answers.LastActivityDate: 2024-09-06T10:34:45.520Z
Answers.UserDisplayName: Rexcirus
Body: <p>Theorem proving is basically a turn-based game with perfect information: you start from a given gamestate (a proposition) and make moves that lead to other valid gamestates. A piece of software can check whether the moves you make are legal and whether you reached a valid solution completing the game.<br />
  That doesn't sound very different from Go, although of course the search space is much larger.</p>
  <p>A similar game seems perfect for RL; for an algorithm like AlphaZero. We could generate an unlimited amount of theorems by combining existing ones (possibly aided by a model trained to generate interesting or difficult theorems), and train a model to solve them.</p>
  <p>In the past years I've followed this field, and I've seen the birth of a bunch of tools (my favorite is LeanDojo), as well as a lot of research (using Lean, Metamath, Agda, Coq, as well as human-generated non-formal proofs). Nevertheless I haven't seen any noteworthy attempt at using Reinforcement Learning in combination with a theorem prover to create a powerful proving model.</p>
  <p>I'm thus wondering whether it's feasible with today's technology to automate Theorem Proving (up to human-level) via Reinforcement Learning?</p>
  <p>If feasible, I'd love to see some research on the problem by respectable organizations. While if it's not, I'd like to understand what the issues are: is it just because the search space is so large, or are there other challenges I can't see?</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2024-03-16T15:12:18.363Z
Comments.Text: I've also wondered about this. Not a mathemetician, but math researchers probably care more about proving or disproving *particular* conjecture than obtaining a huge number of true statements. With that in mind, I expect it will be much harder to evaluate whether a particular state of your theorem prover is close or far to your target theorem than it will be to determine if a particular state of Go is winning or losing. Especially because those regions of state space will not have been explored in existing data (if they were, we might have proved/disproved the theorem already).
Comments.UserDisplayName: bogovicj
Tags: <reinforcement-learning><automated-theorem-proving>
Title: How feasible is it to automate Theorem Proving via Reinforcement Learning?
UserDisplayName: Blue Nebula
ThreadText: # How feasible is it to automate Theorem Proving via Reinforcement Learning?
  
  (Asked by: username_0 on 2024-03-10)
  
  Theorem proving is basically a turn-based game with perfect information: you start from a given gamestate (a proposition) and make moves that lead to other valid gamestates. A piece of software can check whether the moves you make are legal and whether you reached a valid solution completing the game.  
  That doesn't sound very different from Go, although of course the search space is much larger.
  
  A similar game seems perfect for RL; for an algorithm like AlphaZero. We could generate an unlimited amount of theorems by combining existing ones (possibly aided by a model trained to generate interesting or difficult theorems), and train a model to solve them.
  
  In the past years I've followed this field, and I've seen the birth of a bunch of tools (my favorite is LeanDojo), as well as a lot of research (using Lean, Metamath, Agda, Coq, as well as human-generated non-formal proofs). Nevertheless I haven't seen any noteworthy attempt at using Reinforcement Learning in combination with a theorem prover to create a powerful proving model.
  
  I'm thus wondering whether it's feasible with today's technology to automate Theorem Proving (up to human-level) via Reinforcement Learning?
  
  If feasible, I'd love to see some research on the problem by respectable organizations. While if it's not, I'd like to understand what the issues are: is it just because the search space is so large, or are there other challenges I can't see?
  
  **Tags:** reinforcement-learning, automated-theorem-proving
  
  > **Comments:**
  > **username_1**: I've also wondered about this. Not a mathemetician, but math researchers probably care more about proving or disproving *particular* conjecture than obtaining a huge number of true statements. With that in mind, I expect it will be much harder to evaluate whether a particular state of your theorem prover is close or far to your target theorem than it will be to determine if a particular state of Go is winning or losing. Especially because those regions of state space will not have been explored in existing data (if they were, we might have proved/disproved the theorem already).  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_2 on 2024-09-06. Score: 1
  
  It is feasible, even though we are at the level of high-school mathematics at the moment. But there is room for scaling. Examples are:
  
  [HyperTree Proof Search for Neural Theorem Proving (2022)](https://arxiv.org/abs/2205.11491)
  
  [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback
  for Reinforcement Learning and Monte-Carlo Tree Search (2024)](https://www.arxiv.org/pdf/2408.08152)
  
  The first paper use a generalization of AlphaZero, while the second build a much more complex pipeline including supervised training, MCTS and reinforcement learning.
  
  
  ---
  
  