Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?
16
50
Ṁ4.2KṀ330
2025
63%
chance
1D
1W
1M
ALL
Meaning: take a formal language proof and write a natural language proof that is accepted by human judges as correct.
The AI in question does not need to produce the formal proof.
No restrictions on the formal language being used.
Related markets:
Get Ṁ200 play money
Related questions
Will AIs be widely recognized as having developed a new, innovative, foundational mathematical theory before 2030?
29% chance
Will an AI get bronze or silver on any International Math Olympiad by end of 2025?
38% chance
Will an AI solve any important mathematical conjecture before January 1st, 2030?
62% chance
In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)
39% chance
Will an AI get bronze on any International Math Olympiad by 2025?
42% chance
Will an AI be able to convert recent mathematical results into a fully formal proofs that can be verified by a mainstream proof assistant by 2025?
23% chance
Will any AI be able to formalize >=90% of IMO problems by the start of 2025?
32% chance
Will natural language based proof assistants be in common use by 2026?
36% chance