Are there any lean competitions?

Stream: general

[Iván Renison]

Hi, I wanted to ask: do you know if there are any math olympiad style contests in lean?
I have heard that IA is now good at solving math olympiads problems and I wonder if there is a platform like codeforces but for math in lean

[Floris van Doorn]

There is a Lean codewars: https://www.codewars.com/kata/search/lean

[Floris van Doorn]

I'm not sure how maintained that is, the first problem I see is in Lean 3. So it might all be hopelessly outdated.