Topic: Formalised IMO solutions
Adrián Doña Mateo (Mar 29 2021 at 20:11):
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 (Mar 29 2021 at 20:14):
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 (Mar 29 2021 at 20:16):
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 (Mar 29 2021 at 22:56):
Just remember that IMO proofs are not being included for the sake of ticking off the list of IMO problems. We like them because
- 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)
- they are a nice way to draw in new contributors to mathlib, by getting the authors through a first PR process. :-)
Yury G. Kudryashov (Mar 29 2021 at 23:13):
- They can tell us about missing lemmas in
Manuel Candales (Mar 29 2021 at 23:56):
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 (Mar 29 2021 at 23:56):
- 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 (Mar 29 2021 at 23:57):
@Manuel Candales, invitation sent!
Tian Chen (Apr 05 2021 at 19:04):
Hi! I'd like to contribute some problems (IMO 1977/6, 2001/2, 2006/3). My github username is
Floris van Doorn (Apr 05 2021 at 19:15):
Last updated: May 08 2021 at 19:11 UTC