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
)

info: downloading https://releases.lean-lang.org/lean4/v4.19.0/lean-4.19.0-linux.tar.zst


info: installing /home/runner/.elan/toolchains/leanprover--lean4---v4.19.0


✔ [1/9] Built REPL.Frontend


✔ [3/22] Built REPL.Lean.ContextInfo
✔ [4/22] Built REPL.Util.Pickle
✔ [5/22] Built REPL.Util.Path
✔ [6/22] Built REPL.Lean.ContextInfo:c.o


✔ [7/22] Built REPL.Frontend:c.o
✔ [8/22] Built REPL.Util.Pickle:c.o


✔ [9/22] Built REPL.Lean.Environment
✔ [10/22] Built REPL.Util.Path:c.o


✔ [11/22] Built REPL.JSON
✔ [12/22] Built REPL.Lean.Environment:c.o
✔ [13/22] Built REPL.Lean.InfoTree


✔ [14/22] Built REPL.Snapshots


✔ [15/22] Built REPL.Lean.InfoTree.ToJson


✔ [16/22] Built REPL.Lean.InfoTree.ToJson:c.o
✔ [17/22] Built REPL.JSON:c.o


✔ [18/22] Built REPL.Lean.InfoTree:c.o


✔ [19/22] Built REPL.Snapshots:c.o


✔ [20/22] Built REPL.Main


✔ [21/22] Built REPL.Main:c.o


✔ [22/22] Built repl
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.