lean-reinforcement 0.1.4

Reinforcement learning for Lean theorem proving

LeanReinforcement

Repository for LeanReinforcement (LR), a Monte Carlo Tree Search (MCTS) agent building on the ReProver system.

Gym-like

This repository builds on the gym-like LeanDojo interface for interacting with Lean. See the LeanDojo documentation for more information on how to use it.

Monte Carlo Tree Search

Relevant sources will be added here as the project progresses.

TODO

• Import ReProver weights to Snellius
• Set up premise retrieval code
• Create gym environment with LeanDojo and OpenAI Gym
• Decide PPO vs MCTS => MCTS on top of ReProver
• Update Snellius environment
• Import LeanDojo benchmark to Snellius
• Look into LeanDojo step time, value functions, etc.
• Implement runner script to run MCTS agent on LeanDojo environment
• Implement appropriate DataLoader training and evaluation
• Implement training loop
• Run experiments on Snellius
• Finish in-comment ToDo's
  • Checkpoint saving and loading
  • Subtree reusage
  • Reimplement tactic generator fine-tuning
• Implement ValueHead Dataset creation
• Set up wandb/tensorboard equivalent logging
• Write README.md
• Write paper
• Fix parallelization memory issues

License

LeanReinforcement: An MCTS RL agent for Automatic Theorem Proving in Lean. Copyright (C) 2025 Gerben Koopman

This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program. If not, see https://www.gnu.org/licenses/.