# LeanDojo-v2: A Comprehensive Library for AI-Assisted Theorem Proving in Lean

## Framework for Training, Evaluating, and Deploying AI-Assisted Theorem Provers for Lean 4

Ryan Hsiang1, William Adkisson2, Robert Joseph George3, Anima Anandkumar3
1National Taiwan University; 2Washington University in St. Louis; 3California Institute of Technology
Published: NeurIPS Mathematical Reasoning and AI, 2025
Code Paper

## The Updated Library

LeanDojo-v2 is an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4. It combines repository tracing, lifelong dataset management, retrieval-augmented agents, Hugging Face fine-tuning, and external inference APIs into one toolkit.

### Key Features

#### Repository Tracing

Automatically clones Lean repositories (GitHub or local) and traces them with Lean instrumentation to extract theorem information, proof states, and structured data for training.

#### Lifelong Dataset Management

Stores structured theorem information in a dynamic database that keeps repositories sorted by difficulty and appends new theorems without retracing everything.

#### Multiple Agent Types

HFAgent: Uses Hugging Face models fine-tuned locally with SFTTrainer or GRPOTrainer. ExternalAgent: Uses Hugging Face Inference API for large models without local GPU resources. LeanAgent: Implements lifelong learning with retrieval-augmented generation.

#### Flexible Training Options

SFTTrainer: Supervised fine-tuning with LoRA support. GRPOTrainer: Group Relative Policy Optimization for reinforcement learning. RetrievalTrainer: Trains dense retrievers for premise selection.

#### Proof Methods

Supports both whole-proof generation (complete proof in one forward pass) and proof search (sequential tactic generation with state interaction through Pantograph).

#### LeanProgress Integration

Includes support for step-prediction models that estimate remaining proof steps, improving search efficiency through intelligent guidance.

The codebase is modular and extensible! You can implement custom agents by pairing trainers with compatible provers. For detailed documentation and usage examples, visit the GitHub repository.

## Original LeanDojo (Deprecated)

Note: The original LeanDojo library is deprecated. Please use LeanDojo-v2 for all new projects. The information below is kept for historical reference.

### LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Kaiyu Yang 1, Aidan Swope2, Alex Gu3, Rahul Chalamala1, Peiyang Song4, Shixing Yu5,
Saad Godil2, Ryan Prenger2, Anima Anandkumar1 2
1Caltech; 2NVIDIA; 3MIT; 4UC Santa Barbara; 5UT Austin
Published: Neural Information Processing Systems (NeurIPS) 2023
arXiv Code Docs Models Dataset (Lean 3) Dataset (Lean 4)

### Overview

Top right: LeanDojo extracts proofs in Lean into datasets for training machine learning models. It also enables the trained model to prove theorems by interacting with Lean's proof environment.

Top left: The proof tree of a Lean theorem \(\forall n \in \mathbb{N},~\texttt{gcd n n = n}\), where \(\texttt{gcd}\) is the greatest common divisor. When proving the theorem, we start from the original theorem as the initial state (the root) and repeatedly apply tactics (the edges) to decompose states into simpler sub-states, until all states are solved (the leaf nodes). Tactics may rely on premises such as \(\texttt{mod_self}\) and \(\texttt{gcd_zero_left}\) defined in a large math library. E.g., \(\texttt{mod_self}\) is an existing theorem \(\forall n \in \mathbb{N},~\texttt{n % n = 0}\) used in the proof to simplify the goal.

Bottom: Our ReProver model. Given a state, it retrieves premises from the math library, which are concatenated with the state and fed into an encoder-decoder Transformer to generate the next tactic.

## Core Innovation

LeanDojo serves as the foundational infrastructure that bridges the gap between the Python-based world of machine learning and the specialized environment of the Lean prover. It solves the critical data extraction and interaction problems that enable all subsequent research in AI-driven theorem proving.

### Key Capabilities

#### Data Extraction

Systematically extracts rich datasets from Lean repositories, including abstract syntax trees (ASTs), file dependencies, proof states, tactics, and fine-grained premise annotations—essential for training retrieval-augmented models.

#### Interactive Environment

Transforms Lean into a gym-like environment where AI agents can programmatically observe proof states, submit tactics, and receive feedback—indispensable for evaluation, deployment, and reinforcement learning.

## Benchmarks

- LeanDojo Benchmark: 98,734 theorems/proofs, 217,776 tactics, and 130,262 premises from mathlib.
- LeanDojo Benchmark 4: 122,517 theorems/proofs, 259,580 tactics, and 167,779 premises from mathlib4.

LeanDojo can extract data from any GitHub repos in Lean (supporting both Lean 3 and Lean 4). The data contains rich information not directly visible in the raw Lean code, including file dependencies, abstract syntax trees (ASTs), proof states, tactics, and premises.

Key feature 1: Premise information: LeanDojo Benchmark contains fine-grained annotations of premises (where they are used in proofs and where they are defined in the library), providing valuable data for premise selection—a key bottleneck in theorem proving.

Key feature 2: Challenging data split: Splitting theorems randomly into training/testing leads to overestimated performance. LLMs can prove seemingly difficult theorems simply by memorizing the proofs of similar theorems during training. We mitigate this issue by designing challenging data split requiring the model to generalize to theorems relying on novel premises that are never used in training.

## Interacting with Lean

LeanDojo turns Lean into a gym-like environment, in which the prover can observe the proof state, run tactics to change the state, and receive feedback on errors or on proof completion. This environment is indispensable for evaluating/deploying the prover or training it through RL.

## Experiments

We use LeanDojo Benchmark to train and evaluate ReProver. During testing, the tactic generator is combined with best-first search to search for complete proofs. The table shows the percentage of theorem proved within 10 minutes. The \(\texttt{novel_premises}\) spilt is much more challenging than the \(\texttt{random}\) split. On both data splits, ReProver outperforms Lean's built-in proof automation tactic (tidy), a baseline that generates tactics directly without retrieval, and another baseline using GPT-4 to generate tactics in a zero-shot manner.

## Discovering New Proofs and Uncovering Formalization Bugs

We evaluate ReProver on theorems in miniF2F and ProofNet. It discovers 33 proofs in miniF2F and 39 proofs in ProofNet of theorems that did not have existing proofs in Lean. Our proofs have helped ProofNet uncover multiple bugs in the formalization of theorem statements.

## ChatGPT for Theorem Proving

\(a + b + c = a + c + b\)
Stirling's formula
Gauss' summation formula

We build a LeanDojo ChatGPT plugin that enables ChatGPT to prove theorems by interacting with Lean. Compared to specialized LLMs finetuned for theorem proving (e.g., ReProver), ChatGPT can interleave informal mathematics with formal proof steps, similar to how humans interact with proof assistants. It can explain error messages from Lean and is more steerable (by prompt engineering) than specialized provers. However, it struggles to find correct proofs in most cases, due to weakness in search and planning.