Kimina-Prover 72B

Kimina-Prover (preview: April 2025; 72B release: July 10, 2025) is the Numina × Moonshot AI (Kimi team) formal-reasoning model for Lean 4. Trained from Qwen2.5-72B with a large-scale RL pipeline (Kimi k1.5), it pioneered a reasoning-driven paradigm: instead of tree search, it emits one long 'formal reasoning pattern' interleaving informal math with Lean snippets, then a final whole proof — no external search, value function, or process reward model.

It set miniF2F records (80.7% preview; 84% pass@32 / 87.7% pass@1024 for the 72B, beating the ~9x larger DeepSeek-671B at matched budgets) with remarkable sample efficiency, and was the first neural prover to show clean model-size scaling. Distilled 1.5B/7B versions, an autoformalizer, and the Kimina Lean Server are open.

Honest limits: the 72B needs serious GPU hardware (distills are the practical option); RL-trained reasoning traces are long and slow at inference; Lean 4 only; later systems (Goedel-V2, Seed-Prover) pushed benchmarks further.