Hugging Face· PlatformOpen-weight release

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.

From the source

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.

huggingface.co

Announced

14 Aug 2025 12:13 UTC

Detected