Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
Marco Dos Santos, Hugues de Saxcé, Haiming Wang, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu, Jia Li
cs.LO
Apr 29, 2025 · v1
TL;DR
Open-source high-performance Lean server built on the Lean REPL, parallelizing Lean processes for large-scale proof verification.
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.
Problem
Reinforcement learning pipelines for theorem proving require high-throughput verification of Lean proofs, but existing Lean interaction tools are too slow and lack efficient parallelism and caching mechanisms.
Approach
The Kimina Lean Server is built on top of the Lean REPL with server-side parallelism (managing multiple Lean processes) and an LRU caching mechanism that reuses Lean imports across requests. A lightweight Python client enables submitting proof batches and receiving feedback including extracted tactics and tactic states.
Results
On 64 cores, the Kimina Lean Server verifies proofs in 7:56 total time versus 18:01 for leanclient and 12:56 for LeanInteract. Average verification time per proof is 0.051s on 64 cores. Caching reduces total time from 15:28 (non-cached) to 7:56 (cached).
| Project | 8 cores | 16 cores | 32 cores | 64 cores |
|---|
| leanclient | 109:55 | 56:58 | 30:16 | 18:01 |
| LeanInteract | 87:35 | 45:51 | 24:11 | 12:56 |
| Kimina Lean Server | 42:40 | 21:48 | 11:33 | 7:56 |
Verification time comparison across tools (mm:ss)