"Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad" is a report by Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović and Martin Vechev of INSAIT (Sofia University "St. Kliment Ohridski") and ETH Zurich, posted to arXiv as 2503.21934 in March 2025 and revised through version 5 (September 2025). It is the first proof-grading study from the MathArena group, evaluating eight reasoning models on the six problems of the 2025 USA Mathematical Olympiad with expert human graders.
Summary
The authors start from the observation that benchmarks such as MathArena show reasoning models scoring "comparable to top human competitors" on AIME, but "evaluate models solely based on final numerical answers, neglecting rigorous reasoning and proof generation." Existing proof evaluations either rely on formal verification tools such as Lean, cover only constructive proofs, or (Frieder et al.) tested two older non-reasoning models on possibly contaminated problems. USAMO 2025, six proof problems over two days, was chosen because its questions "are challenging, require detailed proofs for full credit, and are uncontaminated."
Method
Each model solved each problem four times, prompted to write a full proof in LaTeX; solutions (without thought traces) were anonymised and converted to PDF. Grok 3 and Gemini-2.5-Pro were added after initial grading and so were not fully anonymous to the judges. The four graders were former national IMO team members or participants in final-stage team selection, trained on three USAMO 2024 problems. Each problem was graded independently by two judges, each judge covering three problems, following the IMO's double-grading model. Since USAMO publishes no official solutions or marking schemes, the team wrote a scheme per problem from Art of Problem Solving forum solutions verified by the graders, scoring each solution out of 7 with partial credit. Judges recorded a justification for every score and classified the first error in each failed solution as logic, assumption, creativity, or algebra/arithmetic.
Results
Table 1 gives average totals out of 42: Gemini-2.5-Pro 10.1, DeepSeek R1 2.0, Grok 3 2.0, Gemini Flash-Thinking 1.8, Claude 3.7 1.5, QwQ 1.2, o1-pro 1.2 and o3-mini 0.9. Gemini-2.5-Pro's 24.4% average came mainly from Problem 1 (6.5 of 7) and Problem 4 (3.5); it produced a solution scoring 6 or above in six of its 24 attempts. Among nearly 175 solutions from the other models, the only perfect 7/7 was a single Grok 3 attempt on Problem 1. Run costs ranged from $0.42 (QwQ) to $203.44 (o1-pro). The authors conclude that "current LLMs remain inadequate for rigorous olympiad-level mathematical reasoning tasks" and suggest that optimisation methods such as GRPO "may currently be insufficient for tasks requiring detailed logical precision."
The most common failure mode was flawed logic (unjustified steps, misreading earlier progress), followed by treating important steps as trivial; o3-mini "frequently skipped essential proof steps by labeling them as 'trivial'." Models showed little creativity, usually attempting the same wrong strategy across all four runs, and, unlike human contestants, "consistently claimed to have solved the problems." Algebraic manipulation was generally strong, with R1 the exception.
An attempt to replace human graders with o3-mini and Claude 3.7, given the marking scheme and a verified solution, found both "consistently overestimating" quality, inflating scores "by a factor of up to 20": for example o3-mini's own 0.9 became 19.5 under o3-mini grading, and QwQ's 1.2 became 23.8.
Qualitative observations
Because reinforcement-learning training extracts rewards from a boxed final answer, models boxed answers even where no final answer was asked for; in one case QwQ, having correctly deduced that all even numbers satisfy Problem 5's conditions, insisted the answer was 2. Models overgeneralised patterns from small cases without proof. Gemini-2.5-Pro frequently cited theorems and sources that the authors could not locate, in every one of its four Problem 6 attempts. OpenAI's models produced the clearest write-ups; Flash-Thinking and QwQ often produced "chaotic and barely interpretable responses."
Key claims
- USAMO 2025, six problems, eight reasoning models, four runs each, two human graders per solution, 7-point scheme with partial credit.
- Gemini-2.5-Pro 24.4% (10.1/42); all other models below 5%; one perfect solution outside Gemini among about 175 attempts.
- LLM judges (o3-mini, Claude 3.7) overestimated scores by up to 20x and are judged unfit to replace human grading.
- Failure modes in order of frequency: logic errors, unjustified assumptions, lack of creativity; arithmetic errors rare except for R1.
- Answer-boxing and pattern overgeneralisation are attributed by the authors to training artifacts.
Provenance
Retrieved 22 September 2026 from the arXiv HTML rendering of version 5 (arxiv.org); the abstract page is arxiv.org. Grading schemes and judge notes are published at github.com/eth-sri/matharena and matharena.ai. Funding acknowledged from the Swiss National Science Foundation, Bulgaria's Ministry of Education and Science (for INSAIT) and the Swiss State Secretariat for Education, Research and Innovation.
Relationships
- supports: MathArena — the USAMO 2025 proof track and its grading procedure.
- supports: AIME (as a model benchmark) — evidence that final-answer performance does not carry over to proof writing.
- related: MathArena: Evaluating LLMs on Uncontaminated Math Competitions (Balunović et al., 2025) — the platform paper that incorporates this study.
- related: AI Benchmarks and Evaluation