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.7.0-rc1 and v4.19.0
- We backport the latest features of Lean REPL to older versions of Lean
📦 Temporary Projects: Easily instantiate temporary Lean environments
- Useful for experimenting with benchmarks depending on Mathlib like ProofNet# and MiniF2F

Quick Start¶

Install the package¶

pip install lean-interact

Install Lean 4 (if not already installed):

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.