DeepSeek Prover V2
View website
Released April 2025, a 671B MoE model (37B active) for formal theorem proving in Lean 4. Achieves 88.9% on MiniF2F-test. Open-weight under MIT license.
At a glance
- Context window
- 164K tokens
- Modalities
- Text Text → Text Text
Pricing by provider
| Provider | Input / 1M tokens | Output / 1M tokens | |
|---|---|---|---|
Novita
|
$0.70 | $2.50 |
Heads up: We do our best to keep these specs & prices accurate. However, cloud costs may fluctuate based on region, usage, and other factors not listed here. These are estimates based on common setups and are for informational purposes only. Always verify current rates & exact specs with the provider before provisioning.
Compare with other models
Estimated prices shown. Actual costs may vary based on context length, batch size, caching, and provider-specific pricing tiers.