Formalised IMO solutions

Stream: general

[Adrián Doña Mateo]

Hi. I have a couple of formalised solutions to IMO problems (2014 Q1 and 2017 Q2) lying around. Would it be useful if I make a pull request to add them to the archive?

[Kevin Buzzard]

Please do! @Alain Verberkmoes is also working on IMO problems right now so you might want to check you're not doing the same ones

[Adrián Doña Mateo]

Great! I am not writing any now. I just have them from a couple of months ago, and I saw that some where being added to mathlib. Hopefuly he's not working on any of those two.

[Scott Morrison]

Just remember that IMO proofs are not being included for the sake of ticking off the list of IMO problems. We like them because

1. they can be nice standalone examples: but as such should be "exemplary" in style (don't worry -- the PR process will help if it's not quite there)
2. they are a nice way to draw in new contributors to mathlib, by getting the authors through a first PR process. :-)

[Yury G. Kudryashov]

3. They can tell us about missing lemmas in mathlib.

[Manuel Candales]

Hi, I am new to Lean, but I'll like to join in on the fun. I formalized IMO 2008 Q2 Part a. Including a substitution lemma commonly used in olympiad inequalities (not sure if that lemma is already in mathlib though). Could someone please give me permission to push it to a new branch. My github is manuelcandales

[Scott Morrison]

4. and provide training material for the IMO grand challenge (which is not a reason for inclusion in mathlib per se, but still valuable!)

[Scott Morrison]

@Manuel Candales, invitation sent!

[Tian Chen]

Hi! I'd like to contribute some problems (IMO 1977/6, 2001/2, 2006/3). My github username is peakpoint.

[Floris van Doorn]

invitation sent!