一键打开：https://gitpod.io/new/#/https://github.com/chenjulang/IMOSLLean4
Formalization & Generalization of IMO Shortlist Problems in Lean 4.
This repo stores formalizations of IMO Shortlist problems from 2006 in every category except Geometry. It also generalizes a few problems with varying degree; for example, see our formalization of IMO 2017 A6 (P2).