This is a prototype of back-and-forth communication with the Lean server through an external program (in this case Python). The goal is to implement a tool for reinforcement learning whereby an external program can query Lean about applying a particular tactic to a particular goal.
The main result this notebook. You should only need Python3 and Jupyter to run it. You also need Lean installed. It assumes you can execute the Lean server via the command lean --server.