Topic: Is this happening in 2020?
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.
Reid Barton (May 23 2020 at 02:00):
The 2020 IMO is (currently?) postponed until September. https://imo2020.ru/
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.
Mario Carneiro (May 23 2020 at 04:22):
My impression was that the grand challenge was not specifically directed at IMO 2020
Kevin Buzzard (May 23 2020 at 07:15):
This was also my impression
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.
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".
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