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

Ryan Hsiang; William Adkisson; Robert Joseph George; Anima Anandkumar

cs.LGNov 6, 2026

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

Authors: Ryan Hsiang, William Adkisson, Robert Joseph George, Anima Anandkumar

Organizations: National Taiwan University · Washington University in St. Louis · California Institute of Technology

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 and researchers to easily fine-tune language models on domain-specific Lean codebases and experiment with LLM-assisted theorem proving without a complex setup.

Figures & tables

Figure 1: Overview of the LeanDojo-v2 architecture

Figure 2: Illustration of a goal-tactic graph

Extension	Purpose
Lean4 (modified)	Downloads and configures Lean4/LeanDojo-v2
LeanDojo	Supports one-click LeanDojo tracing
LeanCopilot	Calls models to complete theorems
Agent-TARS	General agentic AI assistance

Table 1: Lean4Code Extensions

Appendix figures & tables5 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 3: Overview of using LeanDojo in Lean4Code

Figure 4: Input paramater screen for LeanDojo panel

Figure 5: Overview of using LeanCopilot in Lean4Code

Figure 6: Prompting LeanCopilot for tactic suggestions

Lean Theorem Proving

Lean theorem proving uses the Lean proof assistant to construct machine-checked mathematical proofs, often with automated search and language models.

See all 129 papers

Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6LLM Evaluation Lean Theorem Proving
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA
Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning
Mar 25, 2026Arsen ShebzukhovCycle Consistency Autoformalization
Department of Computer Science, Stanford University
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Multi-Agent LLM Systems Automated Theorem Proving

Jun 4, 2026J/K move · Enter open · S save

Evaluation of LLMs for Mathematical Formalization in Lean

Tyson Klingner, Drew Bladek, Escher Crawford, Bohao Chen+5

Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA

LLM Evaluation Lean Theorem Proving LLM Mathematical Reasoning Large Language Model-Guided Theorem Proving

Open paper AskPDF arXiv

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@

k

and refine@

k

metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of

<\

0.01$ per correct proof.

Abstract

Lean Theorem Proving

Explore similar work

Evaluation of LLMs for Mathematical Formalization in Lean

Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics