LeanDojo

LeanDojo is a Python library designed for learning-based theorem provers in Lean. It supports both Lean 3 and Lean 4. The library provides two primary capabilities:

1. Data Extraction: Extracting proof states, tactics, premises, and other relevant data from Lean repositories.
2. Programmatic Interaction: Interacting with Lean programmatically to facilitate machine learning workflows.

Note: This original LeanDojo library is deprecated. For all new projects, please use LeanDojo-v2.

When using LeanDojo for theorem proving and data extraction, be aware of the following technical constraints:

• Repository Compatibility: LeanDojo cannot extract data from or interact with theorems within the official lean4 repository.
• FFI Support: Lean repositories that utilize Foreign Function Interface (FFI), such as LeanCopilot, are currently unsupported.
• Proof Types: LeanDojo does not support term-based proofs or proofs that mix tactics and terms.
• Theorem Extraction Scope:
  • LeanDojo only extracts "syntactic theorems"—Lean constants defined specifically using the theorem or lemma keywords.
  • Constants defined using def are not extracted.
  • Extracted theorems are not guaranteed to be real theorems (they are simply Lean constants of type Prop).

When you run trace on a Lean 4 repository, LeanDojo generates a directory structure where each *.lean file is accompanied by several auxiliary files. These files provide the necessary context for machine learning tasks:

• *.olean: Lean's compiled object file.
• *.dep_paths: Paths of dependencies imported by the current file.
• *.ast.json: Abstract Syntax Trees (ASTs) exported by ExtractData.lean.
• *.trace.xml: The most critical file, containing detailed syntactic and semantic information extracted from Lean (e.g., command nodes, theorem names, tactic sequences, and state changes).

A traced repo is a collection of traced files forming a Directed Acyclic Graph (DAG) via imports. It includes the target repo and the specific dependencies used by it.

Directory Structure (Lean 3)

The root directory is the name of the traced repo. Dependencies are stored in _target/deps/:

• [root]/src: Source files of the target repo.
• [root]/_target/deps/lean/library: Lean's standard library.
• [root]/_target/deps/[dependency_name]: Other dependencies like mathlib.

Directory Structure (Lean 4)

In Lean 4, dependencies are stored in the lake-packages directory instead of _target/deps.

Traced repositories are represented by the lean_dojo.data_extraction.traced_data.TracedRepo class.

LeanDojo facilitates machine learning for theorem proving through a two-step process:

1. Tracing: A Lean repository is traced to extract rich syntactic and semantic information (tactic states, tactics, and premises) that is not readily available in the raw source code. This results in a collection of traced files, repos, and theorems.
2. Dojo Interaction: Once traced, LeanDojo allows an external prover (like an ML model) to interact with a theorem by replacing the original human-written proof with a special repl tactic. This repl tactic reads tactics from the external prover, executes them in Lean, and reports the results back. The resulting environment is called a Dojo.

This workflow allows machine learning models to 'practice' theorem proving by interacting with the Lean environment via the Dojo.

You can use LeanDojo to extract syntactic and semantic information from Lean 4 repositories. This process involves specifying a Git repository URL and a specific commit hash. The trace function will then process the repository and generate a directory containing the source files along with several metadata files that describe the structure and semantics of the Lean code.

To perform a trace, use the LeanGitRepo class to define the repository and the trace function to execute the extraction.

from lean_dojo import LeanGitRepo, trace

# Define the repository with its URL and a specific commit hash
repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f")

# Trace the repository and specify the destination directory
trace(repo, dst_dir="traced_lean4-example")

To build the package and upload it to PyPI, use the hatch tool.

hatch build
hatch publish

Before installing, ensure your system meets the following requirements:

Supported Platforms

• Linux
• Windows WSL
• macOS

Software Dependencies

• Git >= 2.25
• Python: 3.9 <= Python < 3.13
• wget
• elan (Lean toolchain manager)

Environment Variables

To interact with GitHub repositories, you must generate a GitHub personal access token and set it as an environment variable:

• GITHUB_ACCESS_TOKEN: Your GitHub personal access token.

The documentation is generated using Sphinx. To build the HTML documentation locally, navigate to the docs directory and use make.

cd docs && make clean && make html && cd ..