Zulip Chat Archive

Stream: general

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

  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 (Mar 29 2021 at 23:13):

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

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

  1. 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 peakpoint.

Floris van Doorn (Apr 05 2021 at 19:15):

invitation sent!

Last updated: Aug 03 2023 at 10:10 UTC