Zulip Chat Archive

Stream: general

Topic: Formalised IMO solutions


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

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

view this post on Zulip Yury G. Kudryashov (Mar 29 2021 at 23:13):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 29 2021 at 23:56):

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

view this post on Zulip Scott Morrison (Mar 29 2021 at 23:57):

@Manuel Candales, invitation sent!

view this post on Zulip 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 peakpoint.

view this post on Zulip Floris van Doorn (Apr 05 2021 at 19:15):

invitation sent!


Last updated: May 08 2021 at 19:11 UTC