Zulip Chat Archive

Stream: IMO-grand-challenge

Topic: IMO 2019 shortlist


view this post on Zulip Joseph Myers (Sep 23 2020 at 17:29):

As well as the IMO 2020 problems, the IMO 2019 shortlist is also now available (six of the problems there were the IMO 2019 problems). I don't think there should be any particular difficulty writing formal versions of most of the non-geometry problem statements using the definitions currently in mathlib. Most of the geometry problems would need extra definitions added to mathlib to express them cleanly, and writing a formal version of C4 is probably also a fair amount of work. (However, C6, although formulated geometrically, should be straightforward to express using the geometry already in mathlib.)


Last updated: May 06 2021 at 01:57 UTC