---

Why Lean-Runner?

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

• 🛡️ 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.

Getting Started

Check the quick start guide for detailed instructions on how to get started with Lean-Runner.

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.

Project Structure

lean-runner/
├── packages/
│   ├── server/             # FastAPI server implementation
│   │   └── lean_server/
│   │       ├── app/        # API endpoints and server setup
│   │       ├── proof/      # Lean proof execution logic
│   │       ├── manager/    # Proof job management
│   │       ├── config/     # Configuration files and loading
│   │       ├── database/   # SQLite persistence layer
│   │       └── utils/      # Utility functions
│   └── client/             # Python client libraries
│       └── lean_runner/
│           ├── client/     # Sync and async client implementations
│           └── proof/      # Proof data protocol
├── playground/             # Lean workspace with dependencies
└── demo/                   # Example scripts and test files

Contributing

Contributions are welcome! Please feel free to submit issues and pull requests.

License

This project is licensed under the MIT License - see the LICENSE file for details.

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}},
}