Kimina-Prover-72B: A Specialized Theorem Proving Model

Kimina-Prover-72B, developed by Project Numina and Kimi teams, is a 72.7 billion parameter model built upon the Qwen2.5-72B base architecture. Its primary focus is on advanced theorem proving, particularly for competition-style problems within the Lean 4 formal proof system. The model's development involved extensive large-scale reinforcement learning, optimizing its ability to generate and verify mathematical proofs.

Key Capabilities

Formal Theorem Proving: Specialized in generating proofs and solving problems in Lean 4.
High Accuracy: Achieves a notable 84.0% accuracy with Pass@32 on the MiniF2F-test benchmark, indicating strong performance in complex mathematical reasoning.
Reinforcement Learning Optimized: Benefits from large-scale reinforcement learning training, enhancing its problem-solving strategies.

Good For

Automated Theorem Proving: Ideal for tasks requiring automated generation or verification of mathematical proofs.
Lean 4 Development: Particularly useful for researchers and developers working with the Lean 4 proof assistant.
Mathematical Problem Solving: Excels in competition-style mathematical challenges that demand rigorous logical deduction.