mathlib

983cb905 - feat(archive/imo): formalize 1987Q1 (#4731)