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

- Company: Hugging Face (huggingface.co)
- Announced: 2025-07-10T12:54:19+00:00
- Category: new-model
- Subject: Platform
- Models affected: Kimina-Prover-72B, Kimina-Prover-Distill-8B, Kimina-Prover-8B, Kimina-Prover-1.7B
- Source: https://huggingface.co/blog/AI-MO/kimina-prover
- Record: https://forck.live/items/1659-kimina-prover-applying-test-time-rl-search-on-large-formal-reasoning-models

Hugging Face announces the release of Kimina-Prover-72B, a state-of-the-art theorem proving model, along with two distilled variants (8B and 1.7B). The model uses test-time reinforcement learning search and error-fixing capabilities, achieving a 92.2% pass rate on the miniF2F benchmark.

## Evidence

Verbatim from https://huggingface.co/blog/AI-MO/kimina-prover:

> 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).

---

Record: https://forck.live/items/1659-kimina-prover-applying-test-time-rl-search-on-large-formal-reasoning-models
Catalogue: https://forck.live/llms.txt
Feed: https://forck.live/feed.md