Kimina-Prover
A 72B RL-trained theorem prover for Lean 4: 84% on miniF2F, MIT-licensed, with distilled 1.5B/7B versions.
About
Kimina-Prover, from Project Numina and Moonshot AI's Kimi team, is a large language model trained with large-scale reinforcement learning specifically for formal theorem proving in Lean 4. Rather than the traditional tactic tree-search, it uses what the authors call a 'formal reasoning pattern' — one long chain-of-thought interleaving informal mathematical sketches with Lean 4 snippets, ending in a whole proof the Lean compiler can verify. The 72B model, released July 10, 2025, scores 84.0% pass@32 on miniF2F (80.7% pass@8192 in the original preview), beating the ~9x larger DeepSeek-671B at matched budgets.
The release is MIT-licensed and unusually complete: the 72B weights, distilled 1.5B/7B/1.7B provers, a 7B autoformalizer for data generation, the Kimina Lean server used in training, and a rectified miniF2F-test dataset (the model found five wrongly formalized problems in the original). It's the first neural prover to show clear performance scaling with model size, and its sample efficiency — strong even at pass@1 — makes it practical for researchers who can't afford thousands of rollouts. The niche is narrow (Lean 4 formal math), but within it this is the state of the art among open models.
Specs
Context window
Pricing
Free quota
API access
Weights
Released
Benchmarks
- miniF2F-test: 84.0% pass@32, 87.7% pass@1024 (Numina/Kimi-reported for Kimina-Prover-72B)
- miniF2F-test: 80.7% pass@8192 (preview report, arXiv 2504.11354)
- Test-time RL lemma search: 92.2% (Numina/Kimi-reported)
- No independent benchmark replication verified
Provider-reported unless a source says otherwise. Benchmarks are marketing-adjacent by nature — treat them as directional.
Use cases
Trust score — 7/10
Scored 7/10 (verified tier, metrics-v1). Evidence: technical report arXiv 2504.11354 (Apr 2025); 72B weights released Jul 10, 2025 on HF under MIT (license confirmed in HF package metadata); miniF2F scores corroborated across the HF model cards, the paper, and independent prover-comparison surveys. Open weights. Strengths: MIT license, genuinely novel reasoning paradigm, sample-efficient, complete open release (distills, Lean server, rectified benchmark). Docked for: (1) all benchmark figures are author-reported with no independent replication found; (2) research preview with no maintenance commitment, and the 72B needs serious compute. License: MIT.
How the trust score is built
Full methodology →- Adoption · stars/downloads, log-scaled vs peers
- 7.0/10
- Maintenance · recency, releases, issue load
- 6.0/10
- Openness · license + docs
- 9.0/10
- Manual review · sanity read + red-flag check
- 7.0/10
- · Numina & Moonshot AI (Kimi); technical report arXiv 2504.11354 (Apr 2025); 72B weights released 2025-07-10
- · MIT license confirmed in HF package metadata for AI-MO/Kimina-Prover-72B
- · miniF2F: 84.0% pass@32, 87.7% pass@1024 (author-reported); 80.7% pass@8192 in preview report
- · Complete open release: distilled 1.5B/7B, autoformalizer, Kimina Lean server, rectified miniF2F-test