# Hugging Face — Kimina-Prover-RL

- Company: Hugging Face (huggingface.co)
- Announced: 2025-08-14T12:13:01+00:00
- Category: open-weight-release
- Subject: Platform
- Open weights: yes
- Models affected: AI-MO/Kimina-Prover-RL-1.7B, AI-MO/Kimina-Prover-RL-0.6B
- Source: https://huggingface.co/blog/AI-MO/kimina-prover-rl
- Record: https://forck.live/items/1635-kimina-prover-rl

AI-MO released an open-source training pipeline kimina-prover-rl for Lean 4 theorem proving and two open-weight models: a 1.7B-parameter model scoring 76.63% Pass@32 on MiniF2F and a 0.6B-parameter model scoring 71.30% Pass@32, each setting a new state of the art for open-source models in their size.

## Evidence

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

> AI-MO/Kimina-Prover-RL-1.7B, a 1.7B-parameter model that achieves 76.63% Pass@32 on the MiniF2F benchmark — setting a new state of the art for open-source models in this size category
> AI-MO/Kimina-Prover-RL-0.6B, a 0.6B-parameter model that achieves 71.30% Pass@32 on the MiniF2F benchmark — also setting a new state of the art for open-source models in this size category.

---

Record: https://forck.live/items/1635-kimina-prover-rl
Catalogue: https://forck.live/llms.txt
Feed: https://forck.live/feed.md