Will the first AI to get IMO Gold integrate Lean?
23
1kṀ1950
2030
66%
chance

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.

AI
Technical AI Timelines
IMO Grand Challenge
The Lean Theorem Prover
Get
Ṁ1,000
to start trading!
Sort by:

I think it's extremely unlikely that it will integrate multiple proof assistants, so ArbBot will try to keep the sum <= 100%.

Related:

People are also trading

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?
81% chance
Will the "AI get gold on any IMO by the end of 2025" market resolve YES before the 2025 IMO?
1% chance
Will an AI get at least silver on International Olympiad in Informatics (IOI) by end of 2025?
97% chance
AI IMO 2025: How many AI labs announce a Gold performance at the IMO in 2025?
Will an AI win a gold medal on International Math Olympiad (IMO) 2025?
57% chance
Conditional on AI getting at least bronze on the IMO, will it get gold by 2025?
-6% 1d72% chance
Will AI get BOTH gold and either bronze or silver on the IMO by end of 2025?
+5% 1d55% chance
Will an AI publicly accessible before IMO 2025 get the gold medal on it?
14% chance
Will the first AI to get IMO Gold integrate Isabelle?
10% chance
© Manifold Markets, Inc.•Terms + Mana-only Terms•Privacy•Rules