IMO-formalization The aim is to formalize problems of International Mathematical Orimpiad (IMO) by Lean4.