# Kimina-Prover-RL

DevFeed: [Kimina-Prover-RL](<https://devfeed.tech/articles/kimina-prover-rl-6980.md>)

Original publisher: [Read original article](<https://huggingface.co/blog/AI-MO/kimina-prover-rl>)

Author: Thibaut Barroyer; Jonas Bayer; Marina Vinyes; Mert Unsal; Haiming Wang; Xiaohan Lin; MantasBaksys; Junqi Liu; Marco Dos Santos; Flood Sung; Ying; Zhu Zekai; Lujianqiao; Hugues de Saxcé; Ebony Zhang; B

Published: 2025-08-14T12:13:01Z

Content type: article

Language: en

Sources: [Hugging Face - Blog](<https://devfeed.tech/sources/hugging-face-blog.md>)

Topics: [Lean](<https://devfeed.tech/topics/lean.md>), [Open Source](<https://devfeed.tech/topics/open-source.md>), [grpo](<https://devfeed.tech/topics/grpo.md>), [Reinforcement learning](<https://devfeed.tech/topics/reinforcement-learning.md>), [Large Language Model](<https://devfeed.tech/topics/llm.md>), [Benchmark](<https://devfeed.tech/topics/benchmark.md>)

Tags: [benchmark](<https://devfeed.tech/tags/benchmark.md>), [code](<https://devfeed.tech/tags/code.md>), [datasets](<https://devfeed.tech/tags/datasets.md>), [grpo](<https://devfeed.tech/tags/grpo.md>), [open-source](<https://devfeed.tech/tags/open-source.md>), [reasoning](<https://devfeed.tech/tags/reasoning.md>), [reinforcement-learning](<https://devfeed.tech/tags/reinforcement-learning.md>), [training](<https://devfeed.tech/tags/training.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

Kimina-Prover-RL is an open-source training pipeline for formal theorem proving in Lean 4. It uses a structured reasoning-then-generation approach, GRPO reinforcement learning, format-checking rewards, error-correction turns, and high-throughput proof verification through kimina-lean-server. The article also introduces 1.7B- and 0.6B-parameter models evaluated on the MiniF2F benchmark.

## Source excerpt

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.