Kimina-Prover

A specialized formal-reasoning model family for producing Lean proofs.

• Developer / Organization: Project Numina and Moonshot AI / Kimi team
• Category: Proof models & model integrations
• Purpose: Train specialized models for formal mathematical reasoning.
• Key features: Lean proof generation, released model weights, benchmark proofs and a companion Lean server.
• Availability: Model / model-integration project; consult model and code licenses separately
• License: Not verified in the linked source (source (opens in a new tab))
• Website / Source code: https://github.com/MoonshotAI/Kimina-Prover-Preview (opens in a new tab)
• Version: Model: Kimina-Prover-72B; supersedes Preview
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01