DeepSeek-Prover-V2

A specialized model family for generating formal Lean proofs through subgoal reasoning.

• Developer / Organization: DeepSeek AI
• Category: Proof models & model integrations
• Purpose: Generate formal mathematical proofs in Lean.
• Key features: Specialized proof models, recursive subgoal reasoning and released inference examples and weights.
• 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/deepseek-ai/DeepSeek-Prover-V2 (opens in a new tab)
• Version: Model family: V2 (7B and 671B)
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01