AI-MO/Kimina-Prover-Distill-0.6B

AI-MO/Kimina-Prover-Distill-0.6B is a 0.8 billion parameter theorem proving model developed by Project Numina and Kimi teams. It is a distillation of the larger Kimina-Prover-72B, specifically optimized for competition-style problem solving in Lean 4. The model achieves 68.85% accuracy with Pass@32 on the MiniF2F-test benchmark, making it suitable for formal mathematics and proof generation tasks.

Warm
Public
0.8B
BF16
32768
License: apache-2.0
Hugging Face