ProverBench (DeepSeek)
DeepSeek-Prover-V2-671B 59.1% Provers write Lean 4 proofs for 325 formalized problems: 15 from AIME 2024 and 2025 and 310 from textbooks across number theory, algebra, calculus and analysis. Lean checks each proof.
DeepSeek released it with DeepSeek-Prover-V2 on April 30th, 2025. Labs often report only the 15-problem AIME subset as problems solved.
- Made by
- DeepSeek
- Released
- April 2025
- Kind
- Formal proofs
- Level
- University
- Scored
- Checked automatically
- Answers
- Written proof
- Tasks
- All public
- Last in a launch post
- April 2025, dropped before it saturated
- Last model added
- April 2025
DeepSeek-Prover-V2-671B leads with 59.1%
Best score per model as labs report them in their own cards. Labs pick their own settings, so these compare less cleanly than independent runs.
Source: Labs’ model cards
| # | Model | Score | Setting | Date | Source |
|---|---|---|---|---|---|
| 1 | DeepSeek-Prover-V2-671B | 59.1% | Apr 2025 | Lab model card |
Scores over time
All the scores we have, one dot each, so a model tested at several settings appears more than once.
Source: Labs’ model cards
No launch post has listed it since April 2025
Launch posts from every lab that has listed it, one tick per post. Tall colored ticks include it, and short gray ones leave it out.
| Date | Launch post | Score | As the post writes it |
|---|---|---|---|
| Apr 30, 2025 | DeepSeek-Prover-V2-671B | 40 | ProverBench-AIME 24&25, 6 of 15 problems solved (chart) |
One system card reports it
Besides launch posts, we read the system cards, model cards and technical reports labs publish with a release. They report far more, including safety and frontier-risk tests.
| Date | Document | Score | As the document writes it | Section |
|---|---|---|---|---|
| Apr 30, 2025 | DeepSeek-Prover-V2-671B technical report | 59.1 | ProverBench All (325 problems), CoT, sample budget 512 (Table 7). AIME 24&25 subset 6 of 15 solved | Capabilities |
More in Math
- AIME 2026 In use Models solve the 30 integer-answer problems from the 2026 AIME I and II math competitions. Scored by exact answer match. GPT-5.5 100%
- IMO-AnswerBench In use 400 olympiad problems with short verifiable answers, robustified against memorization. Scored by answer match. GLM-5.2 91%
- HMMT 2026 In use Models solve the 33 final-answer problems from the February 2026 Harvard-MIT Mathematics Tournament. Scored by exact answer match. GPT-5.5 98.5%
- PolyMath In use Models solve 9,000 parallel math problems in 18 languages across four difficulty levels, from school math to frontier math. Final answers are checked.
Qwen3.7-Max 86.5% - MathArena (Apex, IMO, USAMO) In use Evaluates models on newly released math competitions after release. Final-answer or human/LLM-judged proof scores. Claude Opus 4.8 81.3%
- MathArena Apex Shortlist In use Models solve 47 hard final-answer problems that MathArena selected from 2025 competitions, where the best models scored about 50% at selection. Scored by accuracy over repeated attempts. GPT-5.5 98.4%