IMO 1998 Q3

Stream: IMO-grand-challenge

[John Rathgeber]

Hi Everyone, I'm a new contributor and I just made a PR to prove Q3 from the 1998 IMO. Here is the link: https://github.com/leanprover-community/mathlib4/pull/32860. I'm very new to this and am open to any/all comments!

[Kim Morrison]

I'm not an expert on IMO problems in Mathlib, but do note that IMO proofs in Mathlib are meant to be "exemplary", like everything else in Archive/, i.e. good examples of Lean code. (That is, the Archive/Imo/ directory is not merely trying to collect solutions to as many IMO problems as possible.)

One important part of this is making sure that all subsidiary facts which are generally useful are actually placed out in the main library, so others to use. I think there is (at least) some amount of that required here. As a trivial example, the product of odd numbers being odd!

[Jason Rute]

Compfiles run by @David Renshaw would likely be a better location. Here is the entry for IMO 1998 P3: https://dwrensha.github.io/compfiles/problems/Compfiles.Imo1998P3.html

[Alex Meiburg]

I left some other suggestions for how to make this more Mathlibb-y style, if that's your goal, on the PR!

[John Rathgeber]

Hi all, thank you very much for the comments and replies! In terms of getting my solution into Mathlib, approximately how much work would you estimate I would have to do to generalize/abstract out my lemmas before my PR gets accepted? The reason I ask is that I am just an undergrad student formalizing an IMO problem as my final project for a class (Formal Proof and Verification taught by Rob Lewis at Brown), and I wasn't planning on spending a lot of time fixing up my code over winter break. Of course, it would be nice to contribute something to Mathlib, but I don't want to make this a large time commitment on my part.

Of course, I am happy to commit my work to the David Renshaw's Compfiles repository, as it seems that I don't have to do much extra work to make a contribution there.

[Johan Commelin]

Glancing over the PR, and looking at the lengths of the proofs towards the end, my guess is that we would like to see quite a lot of modularizing and splitting of reusable components.

So yeah, might be better to target compfiles in that case.

And congrats on formalizing an IMO problem. I hope you had fun, and got a buzz when you completed it (-;

[John Rathgeber]

Thank you! Will do.