Will the first AI to get IMO Gold integrate Lean?
23
1kṀ19502030
66%
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,000 to start trading!
1,000Related questions
Related questions
Will an AI win a gold medal on International Math Olympiad (IMO) 2025?
60% chance
Will an AI get gold on any International Math Olympiad by the end of 2025?
79% chance
Will an AI get gold on this Olympiad by the end of 2025?
Will AI win a gold on IMO before it wins a gold on IOI?
76% chance
An AI model published prior to the 2025 IMO achieves gold medal performance
42% chance
Will an AI win a gold medal on the IOI (competitive programming contest) before 2026?
81% chance
Will the first AI to get IMO Gold integrate Isabelle?
10% chance
Will an AI win a gold medal on the IOI (competitive programming contest) before 2030?
95% chance
Will an AI publicly accessible before IMO 2025 get the gold medal on it?
36% chance
Will the first AI to get IMO Gold integrate Coq?
8% chance