LeanDojo is a Python library designed for machine learning-based theorem proving in the Lean 4 proof assistant. It enables researchers and developers to extract structured data from Lean projects and interact with the Lean environment programmatically, facilitating the development of AI-powered theorem proving tools.

How It Works

LeanDojo leverages a robust data extraction pipeline to parse Lean code, capturing intricate details like proof states, tactics, and premises. This structured data is then used to train and interact with language models, allowing for programmatic control and automation of theorem proving tasks. The library's design focuses on providing a comprehensive interface for machine learning models to understand and manipulate Lean proofs.

Quick Start & Requirements

• Installation: pip install lean-dojo or pip install . from the Git repo.
• Prerequisites: Git >= 2.25, Python 3.9 to < 3.13, wget, elan. A GitHub personal access token is required and should be set as the GITHUB_ACCESS_TOKEN environment variable.
• Documentation: Getting Started, Demo, Full documentation.

Highlighted Details

• Supports data extraction and programmatic interaction with Lean 4.
• Provides datasets for theorem proving research (LeanDojo Benchmark, LeanDojo Benchmark 4).
• Includes related projects like ReProver and a LeanDojo ChatGPT Plugin.
• Cited in NeurIPS 2023 for its work on retrieval-augmented language models for theorem proving.

Maintenance & Community

• Active development with contributions from multiple researchers.
• Discussions and bug reporting are managed via GitHub Issues and Discussions.

Licensing & Compatibility

• The project's license is not explicitly stated in the provided README. Compatibility for commercial use or closed-source linking is therefore undetermined.

Limitations & Caveats

• The README mentions compatibility with Lean 4 v4.3.0-rc2 or later, with a legacy branch available for Lean 3. Ensure the correct Lean version is used.