Examples¶

This page provides practical examples of using LeanInteract in different scenarios. Full example scripts are available in the examples directory of the repository.

Basic Theorem Proving¶

This example demonstrates how to define a simple theorem with a partial proof in Lean using LeanInteract:

from lean_interact import LeanREPLConfig, LeanServer, Command

# Initialize configuration and server
config = LeanREPLConfig()
server = LeanServer(config)

# Define a simple theorem
print(server.run(Command(cmd="""
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ a ih => sorry
""")))

CommandResponse(messages=[Message(end_pos=Pos(column=16, line=2), data='declaration uses `sorry`', start_pos=Pos(column=8, line=2), severity='warning')], sorries=[Sorry(end_pos=Pos(column=22, line=5), goal='case succ\nb a : Nat\nih : a + b = b + a\n⊢ a + 1 + b = b + (a + 1)', start_pos=Pos(column=17, line=5), proof_state=0)], env=0)

Working with Mathlib¶

This example shows how to use Mathlib to work with more advanced mathematical concepts:

from lean_interact import LeanREPLConfig, LeanServer, Command, TempRequireProject

# Create configuration with Mathlib
config = LeanREPLConfig(project=TempRequireProject(lean_version="v4.19.0", require="mathlib"))
server = LeanServer(config)

# Define a theorem using Mathlib's real numbers
print(server.run(Command(cmd="""
import Mathlib

theorem irrational_plus_rational 
  (x : ℝ) (y : ℚ) : Irrational x → Irrational (x + y) := by
  intro h
  simp
  assumption
""")))

CommandResponse(messages=[Message(end_pos=Pos(column=12, line=8), data='Goals accomplished!', start_pos=Pos(column=0, line=4), severity='info')], env=0)

Using Custom REPL Versions¶

This example demonstrates how to use a specific REPL version from a custom repository:

from lean_interact import LeanREPLConfig, LeanServer, Command

# Use a specific REPL version from the official Lean repository
config = LeanREPLConfig(
    repl_rev="v4.21.0-rc3", 
    repl_git="https://github.com/leanprover-community/repl"
)
server = LeanServer(config)

# Check the Lean version
response = server.run(Command(cmd="#eval Lean.versionString"))
print(response.messages[0].data)  # Output: "4.21.0-rc3"

# For interface compatibility issues with custom REPLs,
# use run_dict to communicate directly with the REPL:
result = server.run_dict({"cmd": "#eval Lean.versionString"})
print(result)  # Example raw output from the REPL

"4.21.0-rc3"
{'messages': [{'severity': 'info', 'pos': {'line': 1, 'column': 0}, 'endPos': {'line': 1, 'column': 5}, 'data': '"4.21.0-rc3"'}], 'env': 1}

Real-World Examples¶

For more comprehensive examples, check out the following scripts in the examples directory:

parallelization.py
Shows how to parallelize calls to LeanInteract for faster processing.
proof_generation_and_autoformalization.py
Shows how to use models like DeepSeek-Prover-V1.5 and Goedel-Prover on MiniF2F and ProofNet# benchmarks.
beq_plus.py
Demonstrates how to run the autoformalization BEq+ metric on the ProofNetVerif benchmark.
type_check.py
Shows how to optimize type checking using environment states.
extract_mathlib_decls.py
Demonstrates how to extract declarations from Mathlib in parallel using LeanServerPool.