Skip to content

A Python Interface to Lean 4

Fast, scalable, and easy-to-use

Get Started View on GitHub

What is LeanFlow?

LeanFlow is an easy-to-use, scalable Python interface to Lean 4.
It lets you run Lean code, interact with proofs, and evaluate formal statements from Python. Ideal for researchers in autoformalization, theorem proving, and experimentation.

🚀 Fast & Efficient

LeanFlow is built for efficiency, allowing you to execute large-scale workloads simultaneously with minimal overhead.

😊 Easy to Use

A small, Pythonic API that feels intuitive. Start running Lean in just a few lines of code.

🔄 Flexible Deployment

Use interactive mode for local development or server mode for scalable experiments. Switch between them with a small config change.

🎯 Evaluation Tools

Built-in metrics for autoformalization evaluation: TypeCheck, BEq+, LLM Grader, and more.

Installation

pip install leanflow

Get Started in 3 Lines

The simplest way to run Lean from Python:

from leanflow import SyncREPL

repl = SyncREPL(lean_version="4.24.0", require_mathlib=True)
print(repl.run("#eval 1 + 1"))

That's it! LeanFlow automatically downloads Lean and sets up the environment.

Built for Performance

LeanFlow is built on asyncio for high-throughput parallel execution. The synchronous API shown above is perfect for getting started, scripts, and notebooks. For production workloads with parallel evaluation, see the async API.

Two Ways to Run Lean

Run Lean directly on your machine. Perfect for development and testing. 
from leanflow import SyncREPL

repl = SyncREPL(lean_version="4.21.0")
result = repl.run("def double (n : Nat) := 2 * n\n#eval double 21")
print(result)  # Environment(messages=..., data='42')
Connect to a remote LeanFlow server for shared environments and scalable evaluation. 
from leanflow import SyncClient

client = SyncClient(base_url="http://localhost:8000")
result = client.run("def double (n : Nat) := 2 * n\n#eval double 21")
print(result) # Environment(messages=..., data='42')
Start a server with: `leanflow-serve --config server.yaml`

Evaluation Metrics

LeanFlow includes built-in metrics for autoformalization evaluation, including type checking and semantic equivalence checks:

from leanflow import TypeCheck, BEqPlus

header = "import Mathlib"
thm1   = "theorem infinite_primes (n : Nat) : ∃ p, n < p ∧ Nat.Prime p := sorry"
thm2   = "theorem infinite_primes_alt (k : Nat) : ∃ q, k < q ∧ Nat.Prime q := sorry"

# Type checking
metric = TypeCheck(repl_config={"lean_version": "4.24.0"})
result = metric.compute(thm1, header=header)  
print(result) # True

# Semantic equivalence (BEq+)
metric = BEqPlus(repl_config={"lean_version": "4.24.0"})
result = metric.compute(thm1, thm2, header=header)
print(result) # True

Run evaluations at scale with the CLI:

leanflow-eval --config config.yaml

Learn more about metrics

What's Next?

  • Quickstart

    Get up and running in 5 minutes with our step-by-step guide

    Quickstart

  • User Guide

    Learn about REPL, Server, and CLI in depth

    Documentation

  • API Reference

    Complete reference for all classes and methods

    API Docs

Inspiration & Acknowledgements

This project builds upon the incredible work of the Lean community. We are deeply grateful to the authors of the following projects, which directly inspired LeanFlow:

We highly recommend checking out these projects!

Special thanks to the Lean community, the contributors to Mathlib, and the authors of the Lean REPL, whose tools make this ecosystem possible.

Community & Support