IMO problems

Stream: mathlib4

[Violeta Hernández]

Quick question, do we have a goal of formalizing the entire IMO problem compendium? Or is it more of a "it's nice to showcase a few of these" kind of thing?

[Damiano Testa]

Maybe the goal should be to formalize as few as possible until AI takes over and finishes the rest.

[Violeta Hernández]

But where's the fun in that?

[Damiano Testa]

You can still formalise them, if you want: humans still play chess and go, after all!

[Patrick Massot]

Do you know about https://dwrensha.github.io/compfiles/?

[Violeta Hernández]

Awesome! That makes the bar for contributing much lower.

[Joseph Myers]

I think the mathlib archive should "showcase a few of these" in the sense of "complete sets of solutions for a few competitions". So all 392 past IMO problems, and complete sets of solutions for one or two other competitions that are sufficiently different in syllabus or problem style (e.g. something at undergraduate level). Then compfiles can cover the broader range of many different competitions will similar syllabus and problem style.

Note that IMO solutions in the mathlib archive are - see Archive/Imo/README.md - meant to be good examples of idiomatic Lean code using mathlib APIs, well-factored with anything more generally usable going into lemmas in mathlib proper; they're not about "making sure this result is true" or "enabling the result to be used as a lemma in proving other results in Lean". The output of AlphaProof is very far from being such an example of idiomatic Lean. PRing such a solution is also a good educational exercise for a new contributor interested in learning to contribute to mathlib (humans can learn to write in mathlib style from many fewer reviews than AIs). For that educational purpose it doesn't even matter much whether the mathlib archive already has a solution to the problem in question - a new contributor can always formalize an alternative solution to the same problem, different solutions may well help illustrate different things about using Lean and mathlib.