7

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.

nbro
  • 42,615
  • 12
  • 119
  • 217
Frank Bryce
  • 173
  • 4

1 Answers1

6

Artificial Intelligence for Theorem Proving is an active research area as witnessed by the existence of the AITP conference 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.

Zimm i48
  • 176
  • 2