ProofNet
DeepSeek-Prover-V2-671B 37.1% Only in system cards Provers write formal proofs for 371 undergraduate theorems from analysis, algebra and topology textbooks, each with a formal statement and a natural-language proof. The proof checker grades them.
Originally in Lean 3. Prover reports such as DeepSeek-Prover-V2 use the test split, usually a Lean 4 port. Also used for autoformalization.
In the authors’ words
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.
- Level
- University Undergraduates and entry-level professionals
- Scored
- Checked automatically A program checks the result against an answer key, unit tests or the expected final state.
- Answers
- Written proof
DeepSeek-Prover-V2-671B leads with 37.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.
| # | Model | Score | Setting | Date | Source |
|---|---|---|---|---|---|
| 1 | DeepSeek-Prover-V2-671B | 37.1% | Apr 2025 | Model card |
Scores over time
All the scores we have, one dot each, so a model tested at several settings appears more than once.
Labs report it only in system cards
We read the headline results of 479 launch posts from 51 labs, and none of them list this benchmark. Some system cards do, below.
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 |
|---|---|---|---|---|
| 30 Apr 2025 | DeepSeek-Prover-V2-671B technical report | 37.1 | ProofNet-test, CoT, sample budget 1024 (Table 4). Budget 32 30.5 | Capabilities |
More in Math
- IMO-AnswerBench In use 400 olympiad problems with short verifiable answers, robustified against memorization. Scored by answer match. GLM-5.2 91%
- 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%
- 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%
- 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%
- 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% - USAMO 2026 In use Models write full proofs for the six problems of the 2026 USA Mathematical Olympiad. Judges grade each proof from 0 to 7 against rubrics. GPT-5.5 98.2%