Hugging Face· PlatformNew model

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.

From the source

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

huggingface.co

Announced

10 Jul 2025 12:54 UTC

Detected

03 Aug 2026 21:12 UTC (+389d after)