Kavli Affiliate: Ran Wang
| First 5 Authors: Marco Dos Santos, Haiming Wang, Hugues de Saxcé, Ran Wang, Mantas Baksys
| Summary:
We introduce the Kimina Lean Server, an open-source project that enables fast
and scalable interaction with Lean 4 via a unified REST API, designed as a
simple verifier for reinforcement learning pipelines. Built on top of the Lean
FRO’s LeanREPL, it combines server-side parallelization by managing multiple
Lean REPL processes in parallel, with an LRU caching strategy that reuses Lean
imports across multiple requests. These features help reduce initialization
overhead and allow large-scale batch processing of Lean code. The client-side
interface allows users to submit batches of proofs and receive Lean feedback,
including extracted tactics and tactic states via infotree processing. These
features enable a high-performance, scalable workflow for both interaction and
extraction of proofs, tactics, and tactic states. We open source our
implementation on GitHub.
| Search Query: ArXiv Query: search_query=au:”Ran Wang”&id_list=&start=0&max_results=3