Will the first AI to get IMO Gold integrate Lean?
Plus
21
Ṁ14412030
70%
chance
1D
1W
1M
ALL
This question resolves when an AI first gets IMO Gold. It resolves YES if the system that gets gold uses as a subsystem any piece of code from the Lean community, including any code from the leanprover or leanprover-community GitHub organizations.
This question is managed and resolved by Manifold.
Get
1,000and
3.00
1,0003.00Related questions
Related questions
Will an AI get gold on any International Math Olympiad by the end of 2025?
69% chance
Will AI get at least bronze on the IMO by end of 2025?
82% chance
Will an AI win a gold medal on International Math Olympiad (IMO) 2025?
65% chance
Will an AI win a gold medal on the IOI (competitive programming contest) before 2025?
5% chance
Will the first AI to get IMO gold use formal methods?
70% chance
Will OpenAI o1 (or any direct iteration) get gold on any International Math Olympiad by the end of 2025?
48% chance
Will an AI score 1st place on International Math Olympiad (IMO) 2025?
25% chance
What company or institution will produce the first AI to get IMO gold?
Will AI win a gold on IMO before it wins a gold on IOI?
45% chance
Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
60% chance