Code for training an AI for Lean 3 using Deep Reinforcement Learning.
It consists of multiple agents. One is for generating theorems while the others are trying to solve those. The reward for the theorem generation depends on the performance of the solvers. It is intended to keep the tasks for the solvers manageable. At the current stage, the solvers do not reliably solve non-trivial goals, which is most likely due to limited computational resources and some remaining inefficiencies in the implementation.
The theorems are generated by starting with the goal "Prop" in Lean and applying definitions until all goals are closed. There are also a few additional actions, such as closing the goal by adding the current goal to the hypotheses and applying it. This part of the project is the most mature: it is straightforward to generate a large number of diverse theorems that are not solvable by a fixed set of tactics. As an example, see the lemma set uploaded at: https://github.com/todbeibrot/lemma-set
The solvers can choose from a set of tactics and theorems to make progress on the goal. To increase the amount of training data, they are also given theorems from mathlib and previously solved theorems. The proportion of these additional training sources depends on performance across the different kinds of theorems. As a first action, the solvers can also decide whether to attempt proving the negation of the theorem instead.
For the network: I used a CNN. This choice was mainly pragmatic rather than architectural; a transformer-based model would be a natural alternative. As an embedding, I used a word2vec model trained on data from previous runs.
In order to use the project, you need an instance of lean-gym: https://github.com/openai/lean-gym Replace the file "tactic.lean" with the altered file in the folder "lean-gym" and add the other three files in that folder to the target. You also need a list of theorems and definitions in a "data" folder.
If you are interested in training graphs, models, generated theorems, the word2vec model, or lists of definitions/theorems to use, feel free to leave a message.
For evaluation: I did not develop a working MiniF2F evaluation pipeline for this version. An earlier version reached around 11%. While this leaves significant room for improvement, especially given that many MiniF2F theorems are short, it provides a rough baseline for the approach. Note that detection of sorrys should not be turned off outside of training.