DeepSeek-Prover-V1.5

// Overview

DeepSeek-Prover-V1.5 is a 7-billion-parameter open-weight language model from DeepSeek, built for automated theorem proving in the Lean 4 proof assistant. Introduced in a paper posted to arXiv on August 15, 2024 (2408.08152), it is the direct successor to DeepSeek-Prover-V1 and improves on it across both training and inference. The model is pre-trained from DeepSeekMath-Base 7B with extra specialisation on formal mathematics, then supervised-fine-tuned and refined with reinforcement learning. DeepSeek released three checkpoints — DeepSeek-Prover-V1.5-Base, DeepSeek-Prover-V1.5-SFT, and DeepSeek-Prover-V1.5-RL — all on Hugging Face.

Its two headline ideas are RLPAF and RMaxTS. RLPAF (reinforcement learning from proof assistant feedback) uses the Lean verifier itself as the reward: a proof that type-checks is a success signal, so the model learns directly from the proof assistant rather than from human preference labels. RMaxTS is a variant of Monte-Carlo tree search with an intrinsic-reward-driven exploration strategy; instead of generating a whole proof in a single pass, the model expands a search tree of partial proofs using a truncate-and-resume mechanism, which produces more diverse proof attempts and raises the chance of finding one that closes the goal.

On the standard formal-proving benchmarks, DeepSeek-Prover-V1.5-RL with RMaxTS reaches 63.5% on the high-school-level miniF2F test set and 25.3% on the undergraduate-level ProofNet — state-of-the-art for open-source provers at the time, and a large jump over DeepSeek-Prover-V1 (which scored 50.0% on miniF2F). It was later superseded by DeepSeek-Prover-V2 in April 2025, but the V1.5 weights remain freely downloadable for research and self-hosting.

// Benchmarks

1. miniF2F-test (DeepSeek-Prover-V1.5-RL + RMaxTS)63.5%
2. miniF2F-test (single-pass whole-proof, pass@128)51.6%
3. ProofNet-test (DeepSeek-Prover-V1.5-RL + RMaxTS)25.3%
4. miniF2F-test (DeepSeek-Prover-V1, predecessor baseline)50%

Scores on a 0–100 scale (25-point gridlines); higher is better. Each benchmark links to its published source.

// Strengths

• State-of-the-art open-source results at release: 63.5% on miniF2F-test and 25.3% on ProofNet with RMaxTS tree search, well ahead of DeepSeek-Prover-V1 (50.0% on miniF2F)
• Learns directly from the Lean 4 verifier via RLPAF (reinforcement learning from proof assistant feedback) — the reward is whether a generated proof actually type-checks, not a human preference label
• RMaxTS Monte-Carlo tree search with a truncate-and-resume mechanism generates diverse proof paths and improves discovery, with gains that stay stable across a wide range of sampling budgets
• Hybrid whole-proof and proof-step generation with explicit Lean 4 tactic-state conditioning, combining the speed of single-pass proofs with the robustness of step-by-step search
• Compact 7B dense model (built on DeepSeekMath-Base 7B) that runs on a single GPU, with Base, SFT, and RL checkpoints all openly published
• Open weights under the DeepSeek Model License (commercial use permitted) with MIT-licensed code, enabling self-hosting, fine-tuning, and reproducible research

// Best for

• Automated theorem proving and proof search in the Lean 4 proof assistant
• Formal verification of mathematics — closing goals in Mathlib4-style developments and competition-math formalisations (miniF2F / ProofNet)
• Research on neural theorem proving, RL from verifier feedback, and Monte-Carlo tree search for proof generation
• Generating candidate Lean proofs and tactic suggestions to assist human formalisation work
• A reproducible open-weight baseline for building and benchmarking new formal-reasoning systems
• Self-hosted formal-math experimentation and further fine-tuning under the open license

// How to access

// DeepSeek Prover — every version

The full lineage of the DeepSeek Prover line, newest first. Every version has its own page — click any to compare specs, benchmarks and pricing.