Coq 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.