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

AI summary

Overview

Research area: Machine learning for formal mathematics — specifically tooling and infrastructure for AI-assisted theorem proving in the Lean 4 proof assistant.

Technical level: Intermediate. The paper assumes familiarity with Lean, tactics, and goal states, but its main content is software architecture rather than mathematical theory.

Scope: A workshop paper (MATH-AI) describing LeanDojo-v2, a unified library covering Lean repository data extraction, LLM fine-tuning (supervised and reinforcement learning), proof search, and API-based inference, together with Lean4Code, a VSCodium-based Lean-native code editor that exposes these tools through a graphical interface.

What This Paper Is About

Progress in LLM-based theorem proving for Lean has produced many separate research tools — LeanDojo, ReProver, LeanCopilot, LeanAgent, Pantograph, and others — but each is a standalone project that can become outdated, must be maintained independently, and requires programming expertise to install and configure. This makes the tooling hard to use for mathematicians who want to apply AI to their own domain-specific Lean codebases. The paper's goal is to consolidate these capabilities into one modular library with standardized APIs, and to wrap it in an editor that removes most of the setup burden.

Key Contributions

1. LeanDojo-v2, a unified end-to-end framework. A single software library that combines repository data extraction (abstract syntax trees, dependencies, theorems, proofs, and premises), LLM fine-tuning, proof search, whole-proof generation, AI autocompletion, and LLM-assisted theorem proving, with standardized APIs and abstract base classes (BaseAgent, BaseProver) for extension.

2. A flexible training pipeline with multiple paradigms. Support for LeanAgent's progressive curriculum training on ReProver's premise retriever, HuggingFace supervised fine-tuning of any model using state/tactic pairs, LoRA for parameter-efficient training, and reinforcement learning trainers (GRPO and PPO) with user-definable reward functions such as syntax correctness and proof success.

3. Large-model inference without local fine-tuning. Direct inference through HuggingFace API calls, allowing use of models such as DeepSeek-Prover-V2-671B that are prohibitively large to fine-tune, and removing the need for C++ inference libraries such as CTranslate2 — reported to cut build time from over ten minutes to just a few seconds relative to the LeanCopilot approach.

4. Lean4Code, described as the first Lean-native code editor. Built on VSCodium with the VSCode Lean4 extension pre-downloaded and modified to include LeanDojo-v2 as a configuration folder, plus custom one-click extension panels for LeanDojo tracing, LeanCopilot tactic suggestions, and ByteDance's Agent TARS.

Main Findings

• Fragmentation is the core practical bottleneck: the authors identify that existing tools are separate, research-oriented projects that may be outdated, need nontrivial maintenance, and demand technical expertise that many mathematicians lack.

• Difficulty-stratified progressive training: extracted theorems are categorized into easy, medium, and hard using the 33rd and 67th percentiles of proof length measured in proof steps, and repositories are sorted by their number of easy theorems so training proceeds from easiest to hardest. For multiple repositories, one training run is performed per additional repository.

• Proof search is framed as graph search: each goal state is a node, each tactic is an edge, and the prover traverses a goal-tactic graph until no goals remain. Pantograph serves as both the REPL and the search algorithm, supporting depth-first search and Monte-Carlo tree search; a shortest-path algorithm then reconstructs a minimal-length tactic sequence.

• Two proving modes are supported: step-by-step tactic generation with REPL feedback, and whole-proof generation in a single forward pass of the LLM. Tactic generators can be LeanAgent, a fine-tuned HuggingFace model, or API inference.

• Lean4Code's design choices: VSCodium was chosen because it disables VSCode's default telemetry settings, offers a familiar environment for developers, and retains full access to the VSCode extension marketplace. The LeanDojo panel takes five inputs (project name, GitHub URL, commit hash, GitHub personal access token, and Lean version) and produces a project folder on the desktop containing the cloned repository, LeanDojo-v2, a Python script, a temp folder, and an output folder, with tracing triggered by one button and artifacts dumped into an "out" folder.

• LeanCopilot integration offers two modes: downloading the Byte5 retriever model locally, or entering a HuggingFace token to call DeepSeek-Prover-V2-671B through HuggingFace's default inference provider; the extension then automatically edits the project configuration file and installs dependencies.

• No quantitative evaluation is reported. The paper presents architecture, code examples, and interface descriptions, but does not report benchmark results, proving success rates, or comparisons against other systems.

• Acknowledged limitation: Lean version changes are often not backward compatible; the authors state they will update Lean4Code's built-in Lean4 extension with every major release, and that because LeanDojo-v2 is cloned into the target project, support tracks the Lean 4 version of the latest LeanDojo-v2 release.

Methodology in Plain English

The authors took an engineering-integration approach rather than an experimental one. They surveyed the existing ecosystem of Lean+AI tools and identified two gaps: the tools are scattered and hard to maintain, and they are hard for non-programmers to set up. Their response has two halves.

The first half is a library. A user points LeanDojo-v2 at one or more Lean repositories by GitHub URL or local path; the library extracts structured data from them. That data feeds three training routes: LeanAgent's curriculum-style progressive training, HuggingFace fine-tuning where the model learns to map a proof state to the next tactic (optionally with LoRA to save memory, or with reinforcement learning using GRPO or PPO and a custom reward), or no training at all, using hosted API inference for very large models. Once a model exists, the library proves theorems either step by step — applying tactics and checking the resulting goals through the Pantograph REPL while searching a graph of goal states — or by generating an entire proof in one shot. Because the components are behind abstract base classes, users can swap in their own trainers, provers, or tactic generators.

The second half is an editor. Lean4Code repackages a code editor that already speaks Lean, then adds graphical panels so that tasks requiring command-line work — tracing a repository, installing and configuring LeanCopilot, chatting with an agent — become a few form fields and a button click.

Why This Matters

Impact on research: The paper targets infrastructure rather than a new model or benchmark. Its argument is that lowering the setup cost of fine-tuning on domain-specific Lean codebases lets mathematicians and researchers experiment with LLM-assisted proving in specialized subfields, where pretrained models are noted to struggle with tactic generation on harder problems. Consolidating tools under one maintained API also addresses the maintenance burden of scattered research code.

Real-world applications:

• Mathematicians formalizing their own research areas in Lean who want a model tuned on their specific subfield's lemmas and proof style.
• Researchers comparing training methods (supervised, LoRA, GRPO, PPO) or search strategies through a common interface and code path.
• Educators and students learning Lean in an environment where the extension, dependencies, and Lean project are configured automatically.
• Developers building custom provers on top of the abstract trainer and prover classes, mixing ML and non-ML tactic generators.

Industry relevance: The work sits at the intersection of AI coding assistants and formal verification, where verifiable machine-generated reasoning is valuable. The use of hosted inference APIs for frontier-scale models, and the packaging of agentic assistants like Agent TARS directly into an IDE, reflects broader industry patterns of moving inference off-device and embedding agents into developer tooling.

Future Directions

• Adding support for additional machine learning methods and other proof search algorithms beyond those currently implemented.
• Integrating LeanProgress, a theorem-proving framework that incorporates proof progress prediction, into LeanDojo-v2.
• Integrating more theorem-proving tools into Lean4Code's extension panels.
• Keeping Lean4Code compatible with new Lean releases, given that Lean versions are often not backward compatible, and handing the editor over to community development for public contributions.

Target Audience

Mathematicians who want to apply AI to their own Lean projects without deep programming setup; machine learning researchers working on formal theorem proving who need a maintained, unified pipeline for data extraction, fine-tuning, search, and inference; and tool builders who want an extensible base (through BaseAgent and BaseProver) for constructing new provers or trainers. Readers seeking empirical benchmark comparisons will not find them here — the paper is a systems and tooling contribution.

Authors’ abstract

Building on recent progress in machine learning for formal theorem proving in Lean, we introduce LeanDojo-v2: an end-to-end framework that unifies repository data extraction, LLM fine-tuning, proof search, AI autocompletion, and LLM-assisted theorem proving in a single software library. In addition, we provide Lean4Code, a lightweight IDE that integrates the various features of LeanDojo-v2 through a simple, mathematician-friendly UI. These tools will enable mathematicians…