{"id":"arxiv:2504.21230","kind":"preprint","title":"Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification","authors":["Marco Dos Santos","Hugues de Saxcé","Haiming Wang","Ran Wang","Mantas Baksys","Mert Unsal","Junqi Liu","Zhengying Liu","Jia Li"],"author_count":9,"year":2025,"published":"2025-04-29","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2504.21230","nct_id":null,"source_url":"https://arxiv.org/abs/2504.21230","archive_url":"https://space-kitty.com/papers/arxiv:2504.21230","updated":"2025-12-16","pmid":null,"pmcid":null,"openalex_id":"W4417468671","pdf_url":"https://arxiv.org/pdf/2504.21230","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}