[govg]

https://imo-grand-challenge.github.io/

This is a similar contest where the plan is exactly as you describe - to develop a way to solve formal descriptions in Lean of IMO problem.