I have formalized some of the IMO Shortlist problems in Lean. For some of the problems, this also includes their generalizations. Unfortunately, I do not know how to formalize the problems in the geometry category. Sorry, but geometry gets benched this time!
I will still try to keep the project up to date, but only occasionally.
I am currently not interested in extending the range of formalization outside of the IMO Shortlist.
This is a project that covers several undergraduate math topics in Indonesian. So far, the project has covered topics in abstract algebra, linear algebra, real analysis, and complex analysis.