mathlib3

89ea423d - feat(archive/imo): formalize IMO 2005 Q3 (#6984)

feat(archive/imo): formalize IMO 2005 Q3 (#6984) feat(archive/imo): formalize IMO 2005 Q3 Co-authored-by: Manuel Candales <manuelcandales@gmail.com>