# Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models

DevFeed: [Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models](<https://devfeed.tech/articles/kimina-prover-applying-test-time-rl-search-on-large-formal-reasoning-models-6978.md>)

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

Author: Haiming Wang; Mert Unsal; Xiaohan Lin; MantasBaksys; Junqi Liu; Marco Dos Santos; Flood Sung; Ying; Zhu Zekai; Lujianqiao; Hugues de Saxcé; Thibaut Barroyer; Ebony Zhang; Bolton Bailey; Frederick Pu;

Published: 2025-07-10T12:54:19Z

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>), [Reinforcement learning](<https://devfeed.tech/topics/reinforcement-learning.md>), [Benchmark](<https://devfeed.tech/topics/benchmark.md>), [Large Language Model](<https://devfeed.tech/topics/llm.md>), [Artificial Intelligence](<https://devfeed.tech/topics/ai.md>)

Tags: [agentic](<https://devfeed.tech/tags/agentic.md>), [benchmark](<https://devfeed.tech/tags/benchmark.md>), [deepseek](<https://devfeed.tech/tags/deepseek.md>), [large-language-model](<https://devfeed.tech/tags/large-language-model.md>), [qwen3](<https://devfeed.tech/tags/qwen3.md>), [reasoning](<https://devfeed.tech/tags/reasoning.md>), [reinforcement-learning](<https://devfeed.tech/tags/reinforcement-learning.md>), [rl](<https://devfeed.tech/tags/rl.md>), [test](<https://devfeed.tech/tags/test.md>), [training](<https://devfeed.tech/tags/training.md>)

## AI overview

The article announces Kimina-Prover-72B, a theorem-proving model for Lean 4, along with distilled 8B and 1.7B variants. It describes test-time reinforcement-learning search, recursive lemma composition, and error-directed proof repair. The model achieves a 92.2% pass rate on the miniF2F benchmark.

## Source excerpt

Numina & Kimi Team We're excited to announce the release of Kimina-Prover-72B, our state-of-the-art theorem proving model trained with the Kimi k1.5[1] RL pipeline based on Qwen2.5-72B [2]. Alongside it, we are also releasing two distilled variants: Kimina-Prover-Distill-8B and 1.7B (based on Qwen3-8B and Qwen3-1.7B[3] respectively).