Проблема четырёх красок ещё в 1976 году была решена на ЭВМ. И с тех пор простого "короткого" доказательства не получено. Поворчали немного и успокоились. Решена так решена. - На компе.
Доказательство 1976 года было типичным computer-assisted proof, то есть была написана какая-то программа, которая произвела какой-то перебор, и к ней было приделано полуформальное доказательство, что перебор полный и программа верна.
В 2005 году доказательство (точнее, вариант Робертсона-Сандерса-Сеймура-Томаса 1997 года) было полностью формализовано в Coq и теперь уже является компьютерным.
В 2012 году та же команда формализовала доказательство теоремы Фейта-Томпсона о разрешимости групп нечетного составного порядка. Естественно, пришлось формализовать не только 255-страничное доказательство, но и пару книжек по алгебре и анализу.
