← All papers
First page of Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification

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
Open-source high-performance Lean server built on the Lean REPL, parallelizing Lean processes for large-scale proof verification.
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.

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.

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.

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

Project8 cores16 cores32 cores64 cores
leanclient109:5556:5830:1618:01
LeanInteract87:3545:5124:1112:56
Kimina Lean Server42:4021:4811:337:56
Verification time comparison across tools (mm:ss)