Is this happening in 2020?

Stream: IMO-grand-challenge

[Jason Rute]

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]

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

[Jason Rute]

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]

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

[Kevin Buzzard]

This was also my impression

[Jason Rute]

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

[Jason Rute]

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

[Jason Rute]

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