Can AI grade an olympiad proof? A new study finds substantial gaps
A new preprint evaluates language models on expert-graded USAMO solutions and finds that judging long mathematical proofs remains difficult.
A plausible proof is not necessarily a correct one
Language models are increasingly asked not only to solve mathematics problems but also to assess other people’s solutions. A preprint submitted on October 27 examines that harder second role for olympiad-style proofs: assigning a score to a long natural-language argument and catching the errors that can hide in an otherwise convincing chain of reasoning.
Testing graders against expert judgement
The authors assemble candidate solutions from the 2025 United States of America Mathematical Olympiad (USAMO) and pair them with expert grades. They then test 20 language-model systems across several scoring measures, prompting styles and inference methods. To produce challenging incorrect examples at larger scale, the paper also introduces TROJAN, an iterative self-critique workflow for generating adversarial proofs.
Their central conclusion is cautionary. Even strong models still have considerable room to improve at matching expert assessment of olympiad solutions. The authors propose MABGrader, which treats the discrete score choices as alternatives to be selected using a multi-armed-bandit method. They report a 26.4% improvement in quadratic weighted kappa over their cited ProofGrader baseline and a 14% reduction in grading error. Those are author-reported figures on this dataset, evaluation design and comparison set; the work is an unreviewed preprint.
Why grading is a distinct mathematical-AI problem
Checking a formal proof in a system such as Lean means verifying a precisely encoded statement against explicit rules. Grading a written olympiad proof is different: the grader must infer what a student meant, decide whether each informal step is justified and translate a partial or flawed argument into a score. A fluent explanation can therefore make this task especially treacherous for systems trained to generate plausible text.
The study does not establish that automated grading is ready to replace mathematicians, contest judges or formal verification. It offers a useful benchmark for a more modest question: how close are current language models to reliable proof review when the standard is expert judgement rather than surface plausibility? The released code and dataset should make that question easier for others to test.