Past IMO (Seed-Prover formal set)
Seed-Prover 78.1% Dropped Provers write Lean proofs for 155 past IMO problems, mostly adapted from Compfiles and MiniF2F.
Seed curated this set for the Seed-Prover report.
Made by ByteDance Seed Released Jul 2025 Formal proofs Tasks kept private Last in a launch post Jul 2025 , dropped before it saturated
Last model added Jul 2025
- Level
- Competition The strongest students, in olympiad-style contests
- Scored
- Checked automatically A program checks the result against an answer key, unit tests or the expected final state.
- Answers
- Written proof
1
Model scored in lab cards
1
Launch post lists it, from 1 lab
Seed-Prover leads with 78.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.
- 1 Seed-Prover 78.1%
| # | Model | Score | Setting | Date | Source |
|---|---|---|---|---|---|
| 1 | Seed-Prover | 78.1% | Jul 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.
Reported by the lab in its model card
No launch post has listed it since Jul 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 |
|---|---|---|---|
| 31 Jul 2025 | Seed-Prover | 78.1 | Past IMO (Heavy), 155 problems |
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%