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

Understand

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.