Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification

TL;DR

The paper tackles the need for scalable, high-throughput verification in neural theorem proving by designing Kimina Lean Server, which combines server-side parallelization of Lean REPL processes with an LRU import-cache to reduce initialization overhead. A lightweight Python client enables batch submission and infotree-based data extraction, supporting RL-style proof search workflows. Empirical results show 1.5–2× faster verification than existing tools, strong scalability up to 64 cores, and substantial caching gains, with validation in large-scale Kimina-Prover training on miniF2F. The open-source, Lean-version-compatible architecture lowers integration barriers and provides a practical platform for data extraction and large-scale verification in neural theorem proving.

Abstract

We introduce the Kimina Lean Server, an open-source project designed as a high-performance verifier for reinforcement learning pipelines. Built on top of the Lean REPL (Read-Eval-Print Loop) maintained by the Lean FRO, our server combines server-side parallelism by managing multiple Lean processes in parallel with a Least Recently Used (LRU) caching mechanism that reuses Lean imports across requests. On the client side, a lightweight Python package enables submitting proof batches and receiving Lean feedback, including extracted tactics and tactic states. Together, these features enable a scalable workflow for large-scale verification and data extraction. In our experiments, the Kimina Lean Server outperforms previous Lean interaction tools, achieving a 1.5 to 2 times speedup in verification time. Moreover, its improved efficiency has enabled its use in the large-scale training of state-of-the-art models such as Kimina-Prover. We hope that our open-source project will support the neural theorem proving community and accelerate future progress by enabling efficient large-scale verification and proof data extraction.

Figures (1)

• Figure 1: Architecture of the Kimina Lean Server parallelization and caching.