Kimina-Prover-RL

Back to Articles Kimina-Prover-RL Team Article Published August 14, 2025 Upvote 13 +7 Thibaut Barroyer thibautbar Follow AI-MO Jonas Bayer TBUGTB Follow AI-MO Marina Vinyes mavi88 Follow AI-MO Mert Unsal mertunsal Follow AI-MO Haiming Wang HaimingW Follow AI-MO Xiaohan Lin XiaoHLim Follow AI-MO MantasBaksys MantasBaksys Follow AI-MO Junqi Liu ahhwuhu Follow AI-MO Marco Dos Santos dsantosmarco Follow AI-MO Flood Sung floodsung Follow AI-MO Ying zhenzhe Follow AI-MO Zhu Zekai hehepig166 Follow AI-MO lujianqiao rookiemango Follow AI-MO Hugues de Saxcé desaxce Follow AI-MO Ebony Zhang ebony59 Follow AI-MO Bolton Bailey BoltonBailey Follow AI-MO Frederick Pu UnluckyOrangutan Follow AI-MO Zhengying Liu evariste-liu Follow AI-MO LI Jia liyongsea Follow AI-MO 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 anyone to reproduce our experiments or adapt the setup to their own models and datasets. All information to...