Kimina-Prover-RL: Open-Source Training Pipeline for Lean 4 Theorem Proving Released

An open-source training pipeline for Lean 4 formal theorem proving, called Kimina-Prover-RL, has been released based on the 'reasoning-then-generation' paradigm inspired by DeepSeek-R1.

This pipeline uses the GRPO (Group Relative Policy Optimization) reinforcement learning method and is fully compatible with the open-source Verl framework. It is designed so that the model goes through a natural language reasoning process before generating Lean code, separating planning from execution to enhance explainability and error recovery capability.

The two models released together achieved SOTA on the MiniF2F benchmark in their respective size categories:

• Kimina-Prover-RL-1.7B: Achieved 76.63% on Pass@32
• Kimina-Prover-RL-0.6B: Achieved 71.30% on Pass@32

For efficient training, kimina-lean-server, which supports large-scale parallel verification, and kimina-client, a Python package for it, are also provided. The training dataset used is Kimina-Prover-Promptset, which was created by selecting high-difficulty problems from the existing NuminaMath-LEAN and generating variations via Gemini.