ETH Zurich's 'Proof or Bluff?' finds reasoning models fail proof-based USAMO 2025

Researchers at ETH Zurich’s SRI Lab and INSAIT published “Proof or Bluff?”, an evaluation of eight reasoning models on the six problems of the 2025 USA Mathematical Olympiad, graded by four expert judges — former national IMO team members — rather than by checking a final numerical answer. The problems were sourced and the models tested within hours of the competition’s release to rule out training-data contamination.

The results contrasted sharply with the same models’ reported performance on benchmarks like AIME, where leading reasoning models had scored near the top of the human range. Under full-proof grading, out of a maximum 42 points across the six problems, Gemini 2.5 Pro was the only model to score meaningfully — an average of 10.1 points, or 24.4% — while DeepSeek-R1, Grok 3, Claude 3.7 Sonnet, QwQ, o1-pro and o3-mini all scored under 5%. Among nearly 175 solutions graded from every model except Gemini, only a single Grok 3 attempt earned a perfect mark on one problem.

The paper attributed the gap to specific failure modes rather than a uniform lack of ability: models routinely asserted patterns observed in small cases held generally without proving it, treated critical steps as “trivial” without justification, and — in Gemini 2.5 Pro’s case — fabricated citations to plausible-sounding but nonexistent papers to support unproven claims. The authors also noted that, unlike human competitors, the models almost never expressed uncertainty about whether a solution was correct, and that using other LLMs as automated graders substantially overstated scores, inflating them by up to a factor of 20 relative to the human judges.

The paper’s authors argued the result showed that benchmarks scoring only final answers were overstating the mathematical reasoning of reasoning models, and that rigorous proof generation remained a distinct, largely unsolved capability.