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

arXiv: https://arxiv.org/abs/2504.21230 · HTML: https://mlsanity.com/paper/2504.21230/

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Apr 2025.

## Built on by (most cited first, 18 of 18)

- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://mlsanity.com/paper/2508.04440/) (2025)
- [FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory](https://mlsanity.com/paper/2510.02335/) (2025)
- [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026)
- [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning](https://mlsanity.com/paper/2601.06795/) (2026)
- [FormalEvolve: Neuro-Symbolic Evolutionary Search for Diverse Autoformalization](https://mlsanity.com/paper/2603.19828/) (2026)
- [MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving](https://mlsanity.com/paper/2603.24465/) (2026)
- [Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2604.15839/) (2026)
- [Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs](https://mlsanity.com/paper/2604.18587/) (2026)
- [Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4](https://mlsanity.com/paper/2605.25556/) (2026)
- [The FIL Hypothesis: Inductive Biases Help with Kernel Engineering](https://mlsanity.com/paper/2606.30442/) (2026)
- [TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs](https://mlsanity.com/paper/2607.11258/) (2026)
- [MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement](https://mlsanity.com/paper/2608.14221/) (2026)
- [LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs](https://mlsanity.com/paper/2610.11862/) (2026)
- [Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs](https://mlsanity.com/paper/2610.21881/) (2026)

## Abstract (arXiv)

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.