Kimina-Prover-AI-MO-GGUF

The Kimina-Prover model family—comprising Kimina-Prover-Distill-0.6B, Kimina-Prover-RL-0.6B, Kimina-Prover-Distill-1.7B, and Kimina-Prover-RL-1.7B—are advanced theorem-proving language models developed by Project Numina and Kimi teams for rigorous, competition-style mathematical reasoning in Lean 4. The "Distill" variants (0.6B and 1.7B) are distilled from the much larger Kimina-Prover-72B, leveraging large-scale reinforcement learning to efficiently capture high performance in a smaller size: for example, Distill-0.6B achieves 68.85% Pass@32 on MiniF2F-test, while Distill-1.7B reaches 72.95%. The "RL" versions are fine-tuned further by reinforcement learning for enhanced reasoning ability, with RL-0.6B improving to 71.3% Pass@32 and RL-1.7B attaining up to 76.63% Pass@32, making these models state-of-the-art for formal theorem proving tasks.

Kimina-Prover model family (GGUF Format)

---

Model Files

Kimina-Prover-Distill-0.6B

Kimina-Prover-Distill-1.7B

---

Kimina-Prover-RL-0.6B

Kimina-Prover-RL-1.7B

Kimina-Prover-Distill-8B

---

Quants Usage

(sorted by size, not necessarily quality. IQ-quants are often preferable over similar sized non-IQ quants)

Here is a handy graph by ikawrakow comparing some lower-quality quant types (lower is better):