(теорема Фейта-Томпсона гласит, что любая конечная группа нечетного порядка разрешима. Она была доказана в 60-х и легла в основу программы классификации простых конечных групп)
Это, несомненно, самое значительное достижение в области автоматических проверок математических доказательств до сих пор. Группа исследователей работала над этим результатом в течение 6 лет. Математическая польза от этого конкретного результата, полагаю, близка к нулю. Будущее покажет, какую пользу принесет вся эта область в целом.