Generalizing IMO Shortlist Problems

Stream: new members

[Gian Cordana Sanjaya]

Hello,

I'm not exactly new to Lean but I've only started migrating to Lean 4.

Ι'm interested in formalizing IMO Shortlist problems starting from 2006 in Lean 4. I'm also generalizing some of the problems; for example, IMO 2017 A6 (P2) can be solved over any field, not just the reals. Previously, I did these in Lean 3 (https://github.com/mortarsanjaya/imo-A-and-N; it's archived now) until I decided to actually switch to Lean 4. I'm currently in the process of porting the formalized files in Lean 3. (Some of the files are unfortunately a mess due to my greediness...)

I'm currently hosting the project (https://github.com/mortarsanjaya/IMOSLLean4). However, I'm not familiar with GitHub setup; I might need some help for this. I also want to know if anyone has similar interests. Thank you very much.

(Should I move this thread somewhere as well?)

[David Renshaw]

Wow, that's an impressive collection -- 100 IMO shortlist problems with solutions! (In Lean 3)

I have a similar but smaller repo here: https://github.com/dwrensha/compfiles

[David Renshaw]

It makes me wonder how I would fit shortlist problems into my naming scheme.

[David Renshaw]

My opinion is that we should join forces and host a combined repo under https://github.com/leanprover-community (though I don't have the power to create such a thing).

[Gian Cordana Sanjaya]

Thanks for the compliment :sweat_smile: Unfortunately not all of them are exactly the same problem or a straight-up generalization, but I made sure at least that the statements are equivalent.

David Renshaw said:

My opinion is that we should join forces and host a combined repo under https://github.com/leanprover-community (though I don't have the power to create such a thing).

If there are more people, then that will be very good. Note that my aim is mostly just having these problems formalized and generalize them, so that alone might have been a different goal from the other projects.

[Patrick Massot]

Hosting IMO formalizations was part of the targets of https://github.com/leanprover-community/mathzoo. But the maintainer of that project lost interest, and it was not even ported to Lean 4.

[Eric Wieser]

Porting wouldn't make much sense for mathzoo; there was not even any promise that all the files built in the same version of Lean 3!

[Joseph Myers]

I find olympiad formalizations that aim to be up to the standards of the mathlib archive (whether or not physically located there) much more interesting than the "anything goes" approach of mathzoo. So I'd strongly encourage, in particular, looking carefully for missing mathlib API when doing such formalizations, and adding that API to mathlib (in appropriately general form) as you go along. For algebra and number theory problems, that probably mostly takes the form of small lemmas rather than bigger pieces of theory.

I'd also encourage contributing formalizations of IMO problems to the mathlib archive, even if shortlist problems that aren't IMO problems go somewhere else (I'd be fine with having shortlist problems in the mathlib archive as well, but maybe even if a complete set of all past IMO problems would be a reasonable size to go there, a complete set of shortlist problems would be too big). Conceptually, I think of "mathlib archive" as "any known mathematics not expected to be reused in proofs of other results, formalized to the standards of the mathlib archive with anything reusable going in mathlib proper, and kept up to date with current mathlib", not necessarily restricted to a single repository as long as there's some way to find everything that's conceptually part of the archive and it's genuinely kept up to date.

[Gian Cordana Sanjaya]

You're totally right about the missing APIs. I "worked in hiding" while formalizing those problems in Lean 3; I should look over them again and discuss which ones should be put to mathlib4.

Speaking of which, some of the shortlist problems that I've done are actual IMO problems; for example, IMO 2017 P2 (A6). In fact, my initial motivation for this project was storing any progress I have for a special case of that problem (f : F -> F, where F is a field with char(F) = 2; the char(F) \neq 2 case already has a known solution). I can discuss about modifying those and putting them into mathlib4's archive.

[Kevin Buzzard]

There is clearly an interest in lean formalisation of puzzles like this. Does anyone know who runs AOPS? I wonder if they'd team up with us on this? I know this is a different question to where this work goes and whether it should be used as a way to make mathlib better or an end in itself, which are distinct and complicated questions, but getting AOPS to start linking to lean formalisations would do a lot for visibility of this kind of work.