Kimina-Prover-RL
A slimmed-down training pipeline from Kimina Prover, with core features and full compatibility with verl.
We are happy to introduce kimina-prover-rl, an open-source training pipeline for formal theorem proving in Lean 4, based on a structured reasoning-then-generation paradigm inspired by DeepSeek-R1.
This training pipelinee is a simplified version of the system we used to train Kimina Prover, preserving the key components of the system and offering full compatibility with the open-source Verl framework.
It is released as part of a fork of Verl containing the complete training recipe in recipe/kimina-prover-rl, allowing