LeanInteract

LeanInteract is a Python package designed to seamlessly interact with Lean 4 through the Lean REPL.

Key Features

• 🔗 Interactivity: Execute Lean code and files directly from Python
• 🚀 Ease of Use: LeanInteract abstracts the complexities of Lean setup and interaction
• 💻 Cross-platform: Works on Windows, macOS, and Linux operating systems
• 🔧 Compatibility: Supports all Lean versions between v4.8.0-rc1 and v4.25.0-rc2
  • We backport the latest features of Lean REPL to older versions of Lean (see fork).
• 📦 Temporary Projects: Easily instantiate temporary Lean environments
  • Useful for experimenting with benchmarks depending on Mathlib like ProofNet# and MiniF2F
• 🧾 Data extraction: Extract declarations and info trees for analysis and dataset building.
• ⚡ Incremental + Parallel elaboration: Automatically reuse partial computations from previous commands, and enable Elab.async for faster processing.

Quick Start

Install the package

pip install lean-interact

Install Lean 4 (if not already installed) using the following command coming with LeanInteract:

install-lean

Start using it in your Python scripts

from lean_interact import LeanREPLConfig, LeanServer, Command

# Create a configuration for the Lean REPL
config = LeanREPLConfig(verbose=True)  

# Start the Lean server
server = LeanServer(config)  

# Run a simple Lean theorem
server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id"))

Check out the Installation guide for detailed setup instructions and the User Guide for usage examples.