LeanFlow

A fast, scalable, and easy-to-use Python interface to Lean 4.

LeanFlow lets you run Lean code, interact with proofs, and evaluate formal statements directly from Python.

Why LeanFlow?

• 🚀 Fast & Efficient: Built on asyncio for high-throughput, parallel execution.
• 🔄 Flexible Deployment: Seamlessly switch between Local Mode for development and Server Mode for scalable production workloads.
• 🎯 Evaluation Ready: Includes built-in metrics for autoformalization like TypeCheck and BEq+ (semantic equivalence).

Installation

Install LeanFlow via pip:

pip install leanflow

Install Lean 4

LeanFlow requires Lean 4 to be installed on your system. Check out the official Lean 4 installation guide for installation details.

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Quickstart

1. Run Locally (Development)

The simplest way to start. LeanFlow automatically manages the Lean environment for you.

from leanflow import SyncREPL

repl = SyncREPL(lean_version="4.24.0", require_mathlib=True)

result = repl.run("theorem add_zero_nat (n : Nat) : n + 0 = n := by sorry")
print(result)

2. Run as a Server (Scalable)

For heavier workloads or shared environments, connect to a remote LeanFlow server.

Create a config file (server.yaml):

server:
  host: localhost
  port: 8000
repl:
  lean_version: "4.24.0"

Then, start the server:

leanflow-serve --config server.yaml

And connect from Python:

import asyncio
from leanflow import Client

async def main():
    async with Client(base_url="http://localhost:8000") as client:
        result = await client.run("theorem add_zero_nat (n : Nat) : n + 0 = n := by sorry")
        print(result)

if __name__ == "__main__":
    asyncio.run(main())

🌟 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:

• LeanInteract by Auguste Poiroux
• Rethinking and Improving Autoformalization by Qi Liu
• Kimina by Project Numina

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.

License

LeanFlow is released under the MIT License.