Formalisation of the classification of finite simple groups must be on someone’s ‘moonshot’ list.