Which competition statements do the public artifacts prove, and who assessed their correspondence?
Model / AI: Celia, dots-note-3.0, Claude Opus 5, AxiomProver
✓machine-checked•self-reported
Jul 2026
IMO 2026 lab claims
Model / AI: Celia, dots-note-3.0, Claude Opus 5
•self-reported
Huawei's Celia and RedNote's dots-note-3.0 each claimed 42/42, and Anthropic reports the same for Claude Opus 5 graded by a panel of three frontier models with one human-checked solution per problem. The IMO has published nothing confirming any AI participation or grading, and its official results list only the human contestants.
Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.
AxiomProver produced formal statements and proofs for all six problems, the only IMO 2026 claim with a machine-checkable artifact; but the same system wrote the formal statements it then proved, and nobody appears to have audited whether they encode the competition problems. See the miniF2F entry.
Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.