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.

• 🚀 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).

Install LeanFlow via pip:

pip install leanflow

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

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)

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())

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.

LeanFlow is released under the MIT License.

Disclaimer: This open source project is not an official Huawei product, Huawei is not expected to provide support for this project.