Четыре краски нафиг, там переборное доказательство, и верифицировать по факту нужно программу перебора и сведение к ней.

Вообще с красками занятно, там же для рода > 0 вполне человеческое доказательство, может и для сферы есть человеческое, но не очень-то и надо никому.

Для классификации простых групп наверное надо, вдруг они пропустили чего, там же дофига спорадических; а, например, вполне народнохозяйственный алгоритм проверки изоморфности графов ей пользуется.

А верифицировали много чего уже, теорему Фрейденталя уже очень давно, и дофига всякой базовой гомотопической топологии и алгебраической геометрии, по типу валюативных критериев там. Вот кстати комплексную геометрию не смотрел, вбили ли они уже теорию Ходжа.