Answers.Body: <p>Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the <a href="http://aitp-conference.org/" rel="noreferrer">AITP conference</a> and of many publications on the topic. Some papers are mentioned in this thread: <a href="https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303" rel="noreferrer">https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303</a>. I haven't read these papers myself, so I cannot point you to a paper using <em>reinforcement learning</em> specifically, but given the important activity in this domain, I would be very surprised if it hadn't been attempted.</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-06-28T17:46:48.937Z
Answers.Text: Thanks a bunch! I found a few papers via the links you provided which is what I was looking for.
Answers.UserDisplayName: Frank Bryce
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-06-28T17:59:44.920Z
Answers.Text: For anyone interested, [this paper](https://arxiv.org/pdf/1904.03241.pdf) is essentially what I was looking for.  It has a benchmark, a.k.a. theorems that ought to be proved by the "theorem solver" with success rates for a few architectures they tried out. It also has an environment integration with an existing theorem solver "HOL Light" to build your own RI models against. The repository linked in their paper is [here](https://github.com/brain-research/hol-light).
Answers.UserDisplayName: Frank Bryce
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-06-28T18:15:04.933Z
Answers.Text: An updated paper in which they don't seed their model with human proofs is [here](https://arxiv.org/pdf/1905.10501.pdf).
Answers.UserDisplayName: Frank Bryce
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-06-28T16:15:01.277Z
Answers.LastActivityDate: 2020-06-28T16:15:01.277Z
Answers.UserDisplayName: Zimm i48
Body: <p><a href="https://coq.inria.fr/" rel="noreferrer">Coq</a> exists, and there are other similar projects out there. Further, Reinforcement Learning has made splashes in the domain of playing games (a la Deepmind &amp; OpenAI and other less well-known efforts).</p>
  <p>It seems to me that these two domains deserve to be married such that machine learning agents try to solve mathematical theorems. <strong>Does anyone know of any efforts in this area?</strong></p>
  <p>I'm a relative novice in both of these domains, but I'm proficient enough at both to take a stab at building a basic theorem solver myself and trying to make a simple agent have a go at solving some basic number theory problems. When I went to look for prior art in the area I was very surprised to find none. I'm coming here as an attempt to broaden my search space.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-06-28T20:55:45.077Z
Comments.Text: This question seems to be very similar to https://ai.stackexchange.com/q/7416/2444 and https://ai.stackexchange.com/q/21382/2444. Can you clarify how your question is different from those?
Comments.UserDisplayName: nbro
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-06-29T02:40:13.330Z
Comments.Text: well, I found those questions and they didn't really answer what I was looking for.  Reading the answers, they were answering much different parts of the question.  They are more interested in "is this possible? and if so, how?" and I'm more wondering about prior efforts to do this so I don't have to start from scratch. The answer given was pretty much perfect for me, so I'm glad it worked out.
Comments.UserDisplayName: Frank Bryce
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-06-29T14:03:44.467Z
Comments.Text: [This answer](https://ai.stackexchange.com/a/20400/2444) seems to answer your question. If it answers your question, you should at least upvote it.
Comments.UserDisplayName: nbro
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-08-20T05:51:32.450Z
Comments.Text: i'm just going to leave this here: i hesitate to submit it as an answer since i am not in a position to evaluate the talk, but there is evidence that people are working on it!   https://www.youtube.com/watch?v=2m3zcGPKqws
Comments.UserDisplayName: k.c. sayz 'k.c sayz'
Tags: <reinforcement-learning><automated-theorem-proving><coq>
Title: Has reinforcement learning been used to prove mathematical theorems?
UserDisplayName: Frank Bryce
ThreadText: # Has reinforcement learning been used to prove mathematical theorems?
  
  (Asked by: username_0 on 2020-06-28)
  
  [Coq](https://coq.inria.fr/) exists, and there are other similar projects out there. Further, Reinforcement Learning has made splashes in the domain of playing games (a la Deepmind & OpenAI and other less well-known efforts).
  
  It seems to me that these two domains deserve to be married such that machine learning agents try to solve mathematical theorems. **Does anyone know of any efforts in this area?**
  
  I'm a relative novice in both of these domains, but I'm proficient enough at both to take a stab at building a basic theorem solver myself and trying to make a simple agent have a go at solving some basic number theory problems. When I went to look for prior art in the area I was very surprised to find none. I'm coming here as an attempt to broaden my search space.
  
  **Tags:** reinforcement-learning, automated-theorem-proving, coq
  > **Comments:**
  > **username_1**: This question seems to be very similar to https://ai.stackexchange.com/q/7416/2444 and https://ai.stackexchange.com/q/21382/2444. Can you clarify how your question is different from those?  
  > **username_0**: well, I found those questions and they didn't really answer what I was looking for.  Reading the answers, they were answering much different parts of the question.  They are more interested in "is this possible? and if so, how?" and I'm more wondering about prior efforts to do this so I don't have to start from scratch. The answer given was pretty much perfect for me, so I'm glad it worked out.  
  > **username_1**: [This answer](https://ai.stackexchange.com/a/20400/2444) seems to answer your question. If it answers your question, you should at least upvote it.  
  > **username_2**: i'm just going to leave this here: i hesitate to submit it as an answer since i am not in a position to evaluate the talk, but there is evidence that people are working on it!   https://www.youtube.com/watch?v=2m3zcGPKqws  
  
  ---
  
  ## 1 answers
  
  ### Answer by username_3 on 2020-06-28. Score: 5 | Accepted answer
  
  Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the [AITP conference](http://aitp-conference.org/) and of many publications on the topic. Some papers are mentioned in this thread: <https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303>. I haven't read these papers myself, so I cannot point you to a paper using *reinforcement learning* specifically, but given the important activity in this domain, I would be very surprised if it hadn't been attempted.
  
  > **Comments:**
  > **username_0**: Thanks a bunch! I found a few papers via the links you provided which is what I was looking for.  
  > **username_0**: For anyone interested, [this paper](https://arxiv.org/pdf/1904.03241.pdf) is essentially what I was looking for.  It has a benchmark, a.k.a. theorems that ought to be proved by the "theorem solver" with success rates for a few architectures they tried out. It also has an environment integration with an existing theorem solver "HOL Light" to build your own RI models against. The repository linked in their paper is [here](https://github.com/brain-research/hol-light).  
  > **username_0**: An updated paper in which they don't seed their model with human proofs is [here](https://arxiv.org/pdf/1905.10501.pdf).  
  
  ---
  
  