Coq-Python Theorem Prover

Reinforcement learning agent for proving math theorems, using Coq for proving and Python for reinforcement learning.

Code developed at MIT's Brains, Minds, and Machines Lab, supervised by Dr. Andrzej Banburski. Code authored by Christian Omar Altamirano Modesto, Jessica Shi, Anshula Gandhi, Laura J. Koemmpel, Kevin Shen.

Setup

1. Install Coq v. 8.9.0 (https://coq.inria.fr/opam-using.html)
2. pip3 install pexpect gym numpy

Usage

Run python3 main.py