Этим наблюдением заинтересовались математики, и в 1878 году ими была выдвинута «теорема о четырех красках». Многочисленные попытки доказать ее впоследствии оканчивались провалом — каждый следующий математик находил в предыдущем доказательстве ошибки; наконец, в 1976 году американские ученые Кеннет Аппел и Вольфганг Хакен получили убедительное доказательство, предусматривавшее проверку огромного числа карт, которая была выполнена компьютером. Однако математическая общественность продолжала сомневаться: нет ли в коде программы Аппела и Хакена логических ошибок? Лишь недавно французский ученый Жорж Гонтье и британец Бенджамин Вернер сумели подтвердить справедливость доказательства 1976 года, переведя его на специальный язык программы Coq, которая способна проверить истинность любого изложенного с его помощью логического построения.