Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: Current status?


view this post on Zulip Kevin Lacker (Sep 21 2020 at 21:31):

Hey, I saw today's Quanta article about the IMO grand challenge. It sounds cool. I was wondering what the current status is - are there any teams working on an IMO problem solver with some work in progress? I'd be interested in helping out if there was some group open to outside contributors

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:54):

We are currently very interested in getting a nice collection of IMO problems formalised, both statements and proofs

view this post on Zulip Kevin Lacker (Sep 21 2020 at 21:55):

is there a repo of this stuff somewhere

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:55):

There are a couple of Olympiad problems formalised in mathlib

view this post on Zulip Kevin Lacker (Sep 21 2020 at 21:57):

is there a big list or is it like, the combinatorics ones are in the combinatorics directory, etc

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:57):

https://github.com/leanprover-community/mathlib/blob/master/archive/imo1988_q6.lean

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:57):

There are very few

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:57):

It would be nice to start organising them like that

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:57):

They will all live in the archive directory

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 21:58):

src is for the standard maths library, this is entertainment

view this post on Zulip Kevin Lacker (Sep 21 2020 at 22:01):

i wonder what the very easiest IMO problem to formalize is...

view this post on Zulip Stanislas Polu (Sep 22 2020 at 06:40):

IMO 1972 b2 is quite easy and we chatted about its formalization in general a few weeks ago. I'll make a PR to add to to archive/

view this post on Zulip Stanislas Polu (Sep 22 2020 at 07:08):

Done here: https://github.com/leanprover-community/mathlib/pull/4209

view this post on Zulip Quang Dao (Sep 22 2020 at 10:56):

For some problems that ask you to find a certain object (say IMO 2019 P1 & P4), how would you write the statement in Lean?

view this post on Zulip Johan Commelin (Sep 22 2020 at 10:57):

There has been quite some discussion about that (on this stream) without a satisfactory answer so far

view this post on Zulip Johan Commelin (Sep 22 2020 at 10:59):

@Quang Dao see https://leanprover.zulipchat.com/#narrow/stream/208328-IMO-grand-challenge/topic/How.20to.20help.3F/near/175254384

view this post on Zulip Johan Commelin (Sep 22 2020 at 10:59):

(took some time to find that discussion)

view this post on Zulip Quang Dao (Sep 22 2020 at 11:06):

thanks! this link from the discussion is now unusable: https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/determine.lean

view this post on Zulip Quang Dao (Sep 22 2020 at 11:06):

do you know where it has moved to?

view this post on Zulip Quang Dao (Sep 22 2020 at 11:13):

anyway, I'm trying to find simpler instances in Lean where the problem is "find something". Could you solve a polynomial equation (say a quadratic) in Lean?

view this post on Zulip Miroslav Olšák (Sep 22 2020 at 11:20):

Reposting my list of "find something" answers of shortlisted problems 2006 -- 2018: http://www.olsak.net/mirek/determine-answers.txt

view this post on Zulip Daniel Selsam (Sep 22 2020 at 13:13):

Quang Dao said:

thanks! this link from the discussion is now unusable: https://github.com/IMO-grand-challenge/formal-encoding/blob/master/design/determine.lean

https://gist.github.com/dselsam/da69f929de2d623b4a8b5d8ef8a278f9


Last updated: Aug 05 2021 at 05:09 UTC