AI achieves it first International Mathematical Olympiad (IMO) bronze medal in the calendar year X (anything higher than bronze also counts as bronze). AI achieves its first IMO perfect score in the calendar year Y. This market resolves to Y-X.

In case that some AI is not explicitly tested on IMO, but e.g. it solves a Millennium problem and there is a widespread agreement that it could get IMO perfect score were it tested, this question could be resolved before an explicit IMO test. In case of such a possibly contentious resolution I plan to poll Manifold Moderators and/or experts in the field whether they would agree with that resolution.