IMO 2019 shortlist

Stream: IMO-grand-challenge

[Joseph Myers]

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.)