IMO

Stream: general

[Scott Morrison]

Not sure where to post this (PR reviews, mathlib maintainers, or IMO-grand-challenge), so it goes here.

I wrote a README.md to go in /archive/imo/, giving some advice (and opinions!) about the role of that folder in mathlib. See #8799. Hopefully it is helpful to new contributors of IMO problems. If we merge something like it, I will linkify #imo to point at it.

Please feel free to suggest changes (or just make them directly).

[Scott Morrison]

If anyone thinks it is valuable (and/or wants to write it), it may also be useful to add a paragraph about the status and aspirations of the IMO grand challenge.

[Scott Morrison]

Possibly also useful would be for someone with more direct experience with the IMO than me to write a paragraph or two about prospects for including a more representative slice of IMO problems, and what remains to be done in mathlib before this is possible.