☰
AIMO Proof Pilot Winners Announced
We are pleased to announce the results of the AIMO Proof Pilot and to congratulate our winner: Yi-Chia Chen.
The Proof Pilot asked teams to do something genuinely hard: produce full, Olympiad-style mathematical proofs (rather than just final numeric answers) using only models that are truly open source, for which intermediate checkpoints, training protocols and training data are publicly available. These models are rarely used for this purpose and getting them to produce coherent proofs of any kind is a difficult task.
When we posted the outputs on Kaggle, we cautioned that nobody should be surprised if the results were not very high. Against that backdrop, having six teams successfully produce outputs, and three of them achieve high scores, is very impressive.
The six problems were drawn from the AIMO3 public leaderboard set. They range from National Olympiad hard to IMO medium in difficulty, so they sit a little below a full IMO set. They also do not give complete coverage of all topics and difficulties; we tested a particular set of topic and difficulty combinations rather than the whole space.
As the results show, certain topics seem to be found harder, even by SoTA models. We judged P4 to be an IMO easy combinatorics problem, yet only one of the commercial SoTA models we tested was able to solve it.
Team results
Outputs were posted on Kaggle in an anonymised format (labelled team_N and model_N). As promised, we can now reveal which team was which. Each of the six problems was marked on an IMO-style scale out of 7, with scores restricted to 0, 1, 6 or 7 (giving a maximum total of 42).
All of the team and model outputs can be downloaded from this discussion thread.
| Rank | Team | P1 | P2 | P3 | P4 | P5 | P6 | Total |
|---|---|---|---|---|---|---|---|---|
| 1 | Yi-Chia Chen (team 4) | 7 | 7 | 7 | 0 | 7 | 1 | 29 |
| 2 | Nguyen (team 5) | 7 | 6 | 1 | 0 | 7 | 0 | 21 |
| 3 | Bogo de Chãn (team 3) | 6 | 7 | 0 | 0 | 7 | 0 | 20 |
| 4= | Andreas Bisiadis (team 1) | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| 4= | Just a test (team 2) | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| 4= | Natapong Nitarach (Schwyter) (team 6) | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
To put these scores in context: the strongest of the three baseline models available to teams (OLMo) scored just 1 out of 42 on the same problems. (The other two baselines were significantly weaker, so we did not run them through the full evaluation.) The top teams' scores represent a huge improvement on that starting point.
How the teams compare to frontier models
Alongside the team submissions, we evaluated eight other models on the same six problems, covering both open-weight models run locally and commercial SoTA models. These outputs were graded in an anonymised format through exactly the same process as the team submissions.
| # | Model | Access | P1 | P2 | P3 | P4 | P5 | P6 | Total |
|---|---|---|---|---|---|---|---|---|---|
| 1 | Qwen3.6 35B-A3B | Local | 1 | 1 | 0 | 0 | 0 | 0 | 2 |
| 2 | DeepSeek V4 Flash | Local | 7 | 7 | 6 | 1 | 6 | 0 | 27 |
| 3 | OLMo 3 32B Think | Local | 1 | 0 | 0 | 0 | 0 | 0 | 1 |
| 4 | gpt-oss-120b | Local | 1 | 0 | 0 | 0 | 0 | 0 | 1 |
| 5 | GPT-5.5 Pro (extended reasoning) | Browser | 7 | 6 | 7 | 7 | 7 | 7 | 41 |
| 6 | Claude Opus 4.8 (high effort) | Browser | 7 | 1 | 6 | 0 | 7 | 0 | 21 |
| 7 | Claude Opus 4.8 (high effort) | Claude Code (terminal) | 7 | 7 | 6 | 0 | 7 | 6 | 33 |
| 8 | Gemini 3.1 Pro | Browser | 1 | 6 | 0 | 0 | 7 | 0 | 14 |
This comparison demonstrates the strength of Yi-Chia Chen's result. A score of 29/42 exceeds not just every open-source and open-weight model that we evaluated, but several commercial SoTA models, including Gemini 3.1 Pro and Claude Opus 4.8 (run in browser). It was beaten only by GPT-5.5 Pro and Claude Opus 4.8 (run in Claude Code), both of which have had access to an order of magnitude more compute than was available during the Proof Pilot.
The grading process
Grading full proofs requires human judgement, and we took this seriously. Every output was graded independently by at least two expert human graders, and for some outputs as many as four graders assessed the work, in order to establish consensus on the final grade.
We also had three SoTA commercial models grade every output, allowing us to study how closely AI graders track expert-human judgement:
- CG: GPT-5.5 Pro, run in browser
- CL: Claude Opus 4.8, run in Claude Code in the terminal
- GE: Gemini 3.1 Pro (Preview), run via API
The figure below compares each AI grader's marks against the final human grades across all 84 outputs (14 submissions x 6 problems):
A few observations:
- All three AI graders track the final human grades closely. Exact agreement ranges from 82% (Claude Opus 4.8) to 87% (GPT-5.5 Pro and Gemini 3.1 Pro), and agreement within one mark ranges from 95% to 99%.
- Disagreements are overwhelmingly at adjacent marks (the 0/1 and 6/7 boundaries), where even human graders have to make judgement calls about partial credit or minor deductions.
- Serious disagreements, where an AI grader placed an essentially failed proof (0/1) in the essentially correct band (6/7) or vice versa, were rare: GPT-5.5 Pro did this only once in 84 outputs, Gemini 3.1 Pro three times and Claude Opus 4.8 four times.
- Where the AI graders erred, they tended towards leniency. Claude Opus 4.8 and Gemini 3.1 Pro both over-scored more often than they under-scored. GPT-5.5 Pro was the most balanced, and the only AI grader that never awarded major credit to a proof which humans judged to have made no meaningful progress.
We have made the full grading data available, including a further per-output comparison of whether each script reached the correct final answer (as determined by an LLM parser). You can download the CSV here
Next
We will be producing further analysis of the Proof Pilot soon, including working with the teams on an overall paper to further demonstrate the excellent contributions to open-source development that they have made.
As the name suggests, this evaluation was a pilot, and we are thinking about what future competitions in this direction could look like. We will share more in due course, and the feedback that the community has given throughout this pilot will help to shape it.
Finally, we would like to thank all of the teams for their hard work, and everyone in the community who read the outputs and shared comments. We would encourage everyone to take a look at the teams' very interesting discussion threads, where they explain the things they tried and how they went about achieving such strong performances.