Soft question on online math olympiads

Stream: new members

[Ansar Azhdarov]

Hi! I have a few questions about using Lean in online math olympiads. For context, I come from a competitive programming background. One very nice thing about competitive programming is that there exist platforms like Codeforces where they regularly host online competitions. The reason this is possible is, of course, that the solutions can be checked automatically. Since I learned about Lean I've had this idea of creating a similar platform but for math, however, I am not sure how practical this would be.

For example, is it possible to formalize (certain types of) olympiad problems in "real time"? Is mathlib appropriate for this purpose or would one need to develop some library specialized for olympiad math? How could one go about it and how difficult would it be? Now, I am very new to the subject, so it's difficult for me to judge but I am also very eager about the topic. I tried formalizing solutions to some simple problems and it takes disproportionately long compared to coming up with a solution on paper, but I am wondering if this can be overcome with experience.

P.S. I thought I would provide some reasons why I think having such a platform could be useful. First, it would just be cool to have an online olympiad math community. Second, the submitted solutions could be used for AI training in the IMO Grand Challenge(?) Third, I think high school students would be more willing to learn Lean for the sake of competition and then continue using it in the future(?) Again, I have very limited experience and don't know how strong these points are. I would love to hear your opinion on that.

[Yakov Pechersky]

For lean, there are katas on Codewars, but they are Lean3.

[Ansar Azhdarov]

Oops, I submitted the message before finishing typing it. Let met edit it.

[Ansar Azhdarov]

@Yakov Pechersky thanks for the pointers! Do you know if this was ever popularized somehow? It seems there was not too much activity going on.

[Eric Wieser]

The issue with codewars is that the platform never learnt to run Lean 4 code