Will any AI be able to explain formal language proofs to >=50% of IMO problems by the start of 2025?

23

Ṁ5596Jan 1

48%

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 Ṁ1,000 play money

## Related questions

## Related questions

Will an AI get gold on any International Math Olympiad by the end of 2025?

73% chance

Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?

7% 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?

15% chance

Will any AI be able to formalize >=90% of IMO problems by the start of 2025?

20% chance

Will AI get at least bronze on the IMO by end of 2025?

79% chance

Will an AI score 1st place on International Math Olympiad (IMO) 2025?

30% chance

Will an AI win a gold medal on the IOI (competitive programming contest) before 2025?

27% chance

Will the first AI to get IMO gold use formal methods?

67% 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)

65% chance

Will an AI get bronze or silver on any International Math Olympiad by end of 2025?

80% chance