Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: Is this happening in 2020?


view this post on Zulip Jason Rute (May 23 2020 at 01:32):

Assuming the actually Math IMO goes ahead this year, will the IMO Grand Challenge also happen? If so, will there be formal rules at some point? Here are some questions I have:

Is there any consensus about what version of Lean will be used? Lean 4, Lean 3 community (latest version?), or official Lean 3.4.2? (Similar questions about mathlib.)

Is there any consensus about the form of the problems? Can one expect that every proplem will be presented as a prop to prove? (Or is it even up in the air whether every problem will be a prop? For example, will the agent ever need to supply a witness?) Also, is there anything more specific about how certain problems will be presented? Will there be examples of previous problems supplied?

Is the thought still that this will be a community effort more than a competition? If so, is anyone coordinating that effort?

I know you, @Daniel Selsam , were scheduled to talk at the postponed AITP this year. I assume more details would have been presented then.

view this post on Zulip Reid Barton (May 23 2020 at 02:00):

The 2020 IMO is (currently?) postponed until September. https://imo2020.ru/

view this post on Zulip Jason Rute (May 23 2020 at 04:21):

Sorry. I should clarify. I did see the IMO was postponed, but I’m still curious about the grand challenge itself. It’s not clear to me that even with the delay if there is enough time.

view this post on Zulip Mario Carneiro (May 23 2020 at 04:22):

My impression was that the grand challenge was not specifically directed at IMO 2020

view this post on Zulip Kevin Buzzard (May 23 2020 at 07:15):

This was also my impression

view this post on Zulip Jason Rute (May 23 2020 at 11:14):

I got the impression that it will happen over many years (until solved). I'm not clear when it will start.

view this post on Zulip Jason Rute (May 23 2020 at 11:17):

Oh, I see in a previous conversation Daniel says that he doesn't "expect any submissions until 2021 at the earliest".

view this post on Zulip Jason Rute (May 23 2020 at 11:38):

I guess I won't be submitting anything this year. :mischievous:


Last updated: Aug 05 2021 at 05:09 UTC