This market resolves to N, where N is the number of distinct AI labs that have an AI system that meets ALL of these criteria in 2025:
The AI system completes the official 2025 International Mathematical Olympiad problems under standard IMO time constraints (4.5 hours per 3-problem session)
The system was not trained on IMO 2025 solutions (lol). This likely means the system's training was completed before the first day of the IMO 2025.
Humans do not assist with the problem solving of the problems. They can however provide a formal proof language version of the problem.
The system provides complete mathematical proofs (either in natural language or in formal proof languages like Lean), and the natural language proofs are judged to a similar standard as human participants.
The system achieves a score that meets or exceeds the 2025 IMO Gold medal cutoff
Update 2025-28-01 (PST) (AI summary of creator comment): Update from creator
Market close date has been pushed back to allow for valid announcements within a month after the competition.
Announcements made more than a month after the competition will still be counted, potentially requiring the market to be reresolved.
1,000
3.00@AdamK i pushed back the close date. hmmm i guess i could do within a month of the competition, but if someone announces gold a month and a day later, it still counts and gets reresolved? idk, better if there's less waiting but also i wouldn't wanna not count a lab that did achieve this