Skip to content

Home

GitHub Lean Server Lean Runner Docker

Python3.12 Lean 4 Mathlib FastAPI License


  • Plug & Play

    Get started in minutes with Docker's one-click server setup. Our intuitive client abstracts away complex implementation details, letting you focus on what matters—your Lean proofs.

  • High Performance

    Leverages REPL-based atomized execution with fully asynchronous, multi-threaded architecture to maximize CPU utilization and throughput. Efficient interaction with the client using FastAPI.

  • Robust & Reliable

    Persistent SQLite logging ensures your work is never lost. Built-in crash recovery and automatic retry mechanisms eliminate the frustration of interrupted workflows.

  • Flexible Access Patterns

    Choose between synchronous and asynchronous clients depending on your use case, from interactive development to large-scale batch processing.

  • Smart Caching

    Intelligent content-based hashing ensures identical Lean code is processed only once, dramatically reducing computation time for repeated operations.

  • Data Export & Visualization (Soon)

    Easily export data in various formats (Hugging Face, JSON, XML, Arrow, Parquet) and visualize queries with a simple CLI.

Why Server-Client?

Lean-Runner leverages a powerful Server-Client architecture that smartly places all the complex configuration on the server side, while keeping the client implementation elegantly minimal. We've packaged the entire server using Docker, making deployment incredibly straightforward and hassle-free.

Why Async?

Lean-Runner's asynchronous architecture uses a single centralized controller to manage multiple REPL processes, unlike traditional systems that distribute requests across multiple controllers. This design delivers superior performance through concurrent execution, better resource utilization, and direct communication channels. The centralized approach reduces overhead, and enables intelligent load balancing. This scalable architecture allows you to dynamically add more REPL processes as needed, making it perfect for both interactive development and large-scale batch processing of Lean proofs.

Citation

@misc{fanyi2025leanrunner,
    title={Lean-Runner: Deploying High-Performance Lean 4 Server in One Click},
    author={Fanyi Pu, Oscar Qian, Jinghao Guo, Bo Li},
    year={2025},
    publisher={GitHub},
    howpublished={\url{https://github.com/EvolvingLMMs-Lab/lean-runner}},
}