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.