Examples

This page provides practical examples of using LeanInteract in different scenarios. You can find the full examples 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
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(start_pos=Pos(column=8, line=2), end_pos=Pos(column=16, line=2), data="declaration uses 'sorry'", severity='warning')], env=0, sorries=[Sorry(start_pos=Pos(column=17, line=5), goal='case succ\nb a : Nat\nih : a + b = b + a\n⊢ a + 1 + b = b + (a + 1)', proof_state=0, end_pos=Pos(column=22, line=5))])

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
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(start_pos=Pos(column=0, line=4), end_pos=Pos(column=12, line=8), data='Goals accomplished!', 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"

# If you encounter interface compatibility issues with custom REPLs,
# you can 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:

1. proof_generation_and_autoformalization.py
   Shows how to use models like DeepSeek-Prover-V1.5 and Goedel-Prover on MiniF2F and ProofNet# benchmarks.

2. beq_plus.py
   Demonstrates how to run the autoformalization BEq+ metric on the ProofNetVerif benchmark.

3. type_check.py
   Shows how to optimize type checking using environment states.