Elamur Research⌕
☰
home / papers / 2025 / Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification

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

Paper · 2025 · Marco Dos Santos, Hugues de Saxcé, Haiming Wang et al.

Summary

Reinforcement learning for neural theorem proving rewards models based on whether their Lean 4 proofs check, so training depends on verifying very large numbers of proofs quickly. Earlier Python–Lean interfaces often run on a single core or pay a heavy startup cost, mostly from loading Mathlib, for every proof. The Kimina Lean Server is an open-source verifier built on the official Lean REPL from the Lean FRO. It exposes a REST API and keeps a pool of single-threaded REPL processes, one per CPU core, sending each proof to whichever worker is free. Import headers act as keys in an LRU cache, so a worker that has already loaded the same imports only needs to check the body of the proof. A small Python client sends proofs in batches through one check call. It can also turn Lean's infotree into non-overlapping tactics paired with tactic states, which suits tree-search training data. On NuminaMath-LEAN, the server runs 1.5–2× faster than leanclient and LeanInteract. It also served as the verification engine for training Kimina-Prover, which matters for scalable AI-for-math work.

Key points

  • Benchmark: 9,419 valid, sorry-free proofs from NuminaMath-LEAN, run on a GCP C4 VM (5th-gen Intel Xeon) with Lean v4.15.0.
  • Comparison with other tools: At 8 cores the server needed 42:40, against 87:35 for LeanInteract and 109:55 for leanclient. At 64 cores it needed 7:56, against 12:56 and 18:01.
  • Scaling: Going from 8 to 32 cores cut the total time from 42:40 to 11:33, close to a 4× gain. Average time per proof fell from 0.272 s to 0.051 s at 64 cores.
  • Caching: With 64 cores, LRU import reuse reduced the average time per proof from 0.099 s to 0.051 s (1.94×). Total time dropped from 15:28 to 7:56.
  • Use and compatibility: The server was used in RL training of the Kimina-Prover models, which set state-of-the-art results on miniF2F. It works with any Lean version the REPL supports. The code is at github.com/project-numina/kimina-lean-server, and the client is distributed as a PyPI package.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Marco Dos Santos, Hugues de Saxcé, Haiming Wang, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu and Jia Li. 2025. Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification. arXiv:2504.21230.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2504.21230 · arXiv 2504.21230

@misc{santos2025kimina,
  title = {{Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification}},
  author = {Marco {Dos Santos}, Hugues {de Saxcé}, Haiming Wang, Ran Wang, Mantas Baksys, Mert Unsal, Junqi Liu, Zhengying Liu and Jia Li},
  year = {2025},
  doi = {10.48550/arxiv.2504.21230},
  eprint = {2504.21230},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2504.21230}
}

References

12 references, 7 of them with a card of ours. ↗ leads to the work.

  1. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. In Arie Gurfinkel and Marijn Heule, editors, Tools and Algorithms for the Construction an…
  2. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025.
  3. Oliver Dressler. leanclient: Python client to interact with the lean4 language server, 1 2025. URL https://github.com/oOo0oOo/leanclient. ↗
  4. Lean Community. Mathlib Port Status, 2023. URL https://leanprover-community.github.io/mathlib-port-status/. ↗
  5. Lean FRO. A read-eval-print-loop for Lean 4. https://github.com/leanprover-community/repl, 2023. ↗
  6. Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. ISBN 978-3-030-…
  7. Auguste Poiroux, Viktor Kuncak, and Antoine Bosselut. LeanInteract: A Python Interface for Lean 4, 2025. URL https://github.com/augustepoiroux/LeanInteract. ↗
  8. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
  9. Amitayush Thakur, George Tsoukalas, Greg Durrett, and Swarat Chaudhuri. proofwala: Multilingual proof data synthesis and theorem-proving, 2025. URL https://arxiv.org/abs/2502.04671. ↗
  10. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Lo… — Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
  11. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Neural Information Processing Systems (NeurIPS), 2023.
  12. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/santos-2025-kimina-lean-server-high-performance/