Skip to content

Getting Started with LeanInteract

This guide will help you take your first steps with LeanInteract and understand its core concepts.

Overview

LeanInteract provides a Python interface to the Lean 4 theorem prover via the Lean REPL (Read-Evaluate-Print Loop). It enables you to:

  • Execute Lean code from Python
  • Process Lean files
  • Interact with proofs step by step
  • Save and restore proof states

Quick Example

Here's a minimal example to help you get started:

from lean_interact import LeanREPLConfig, LeanServer, Command

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

# Start a Lean server with the configuration
server = LeanServer(config)

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

# Print the response
print(response)

Build completed successfully.
CommandResponse(env=0)

This will:

  1. Initialize a Lean REPL configuration
  2. Start a Lean server
  3. Execute a simple Lean theorem
  4. Return a response containing the Lean environment state and any messages

Understanding Core Components

Let's break down the key components:

LeanREPLConfig

LeanREPLConfig sets up the Lean environment:

config = LeanREPLConfig(
    lean_version="v4.19.0",  # Specify Lean version (optional)
    verbose=True,            # Print detailed logs
)

Build completed successfully.

LeanServer

LeanServer manages communication with the Lean REPL:

server = LeanServer(config)

A more robust alternative is AutoLeanServer, which automatically recovers from (some) crashes:

from lean_interact import AutoLeanServer
auto_server = AutoLeanServer(config)

Commands

LeanInteract provides several types of commands:

  • Command: Execute Lean code directly
  • FileCommand: Process Lean files
  • ProofStep: Work with proofs step by step using tactics

Basic command execution:

response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id"))

Next Steps

Now that you understand the basics, you can:

Or check out the API Reference for detailed information on all available classes and methods.