Primary evidence
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearchS1 · Primary research · Paper · 2024-08-15
- DeepSeek-Prover-V1.5 repositoryS1 · Primary research · Repository
DeepSeek-Prover-V1.5 combines proof-assistant feedback, reinforcement learning and tree search
The model was specialized for Lean 4 formal mathematics, refined with reinforcement learning from Lean feedback and paired with an intrinsic-reward Monte Carlo tree-search variant to explore diverse proof paths. DeepSeek released model weights and code for reproducing the proof-search setup.
What happened?
DeepSeek-Prover-V1.5 reported 63.5% success on miniF2F-test and 25.3% on ProofNet using reinforcement learning from proof-assistant feedback plus RMaxTS proof search, improving on the earlier DeepSeek-Prover line.
Why it matters
The system is a clear bridge from static proof generation toward learned agents that train and search against a formal verifier, while remaining small enough and open enough to become a widely reusable research baseline.
Significance rationale: DeepSeek-Prover-V1.5 made proof-assistant feedback a training signal through reinforcement learning and combined it with Monte Carlo tree search, while releasing the 7B model and proof-search implementation openly.
Historical context
Earlier developments
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic
- AI contribution
- The language model generated Lean proofs and tree-search actions, while Lean supplied correctness feedback for both training and inference-time verification.
- Human contribution
- Researchers assembled formal training data, designed reinforcement-learning and RMaxTS procedures, trained the models and selected benchmark protocols.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- deepseek-prover-v1-5, lean
- Organizations
- deepseek-ai
- Problems
- minif2f, proofnet
- Methods
- reinforcement-learning-from-proof-feedback, monte-carlo-tree-search, formal-theorem-proving, proof-search
Sources & artifacts
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearchS1 · Primary research · Paper · accessed 2026-09-10
- DeepSeek-Prover-V1.5 repositoryS1 · Primary research · Repository · accessed 2026-09-10
- DeepSeek-Prover-V1.5 models and prover codeArtifact · Code
Verification history
- 2024-08-15 · Paper released · E2 · Research record
The paper reported the training method and benchmark results.
- 2024-08-15 · Paper released · E3 · Inspectable artifact
Model weights, Lean integration and proof-search code were released publicly.
Corrections
No corrections recorded.