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

AI-MO/Kimina-Prover-Distill-8B is an 8 billion parameter theorem proving model developed by Project Numina and Kimi teams. This model is a distillation of the larger Kimina-Prover-72B, trained using large-scale reinforcement learning. It specializes in competition-style problem solving within Lean 4, achieving 77.86% accuracy with Pass@32 on the MiniF2F-test benchmark. Its primary strength lies in formal mathematics and automated theorem proving.