ТЧК была сформулирована Фрэнсисом Гутри в 1852 году. Им было высказано предположение, что любую географическую карту, изображенную на листе бумаги, можно раскрасить в четыре цвета таким образом, чтобы страны, имеющие общую границу, были раскрашены в разные цвета. Последовавшие за этим попытки математиков обосновать эту догадку более столетия оказывались безуспешными. Вместе с тем развитие математики породило у многих математиков конца XIX века уверенность в том, что на любой вопрос, сформулированный на языке математики, может быть дан ответ, если будут использованы достаточно мощные математические идеи, и что любой компетентный математик может проверить правильность решения задачи в разумный промежуток времени. Однако полученные в 30-е годы XX столетия К. Геделем и А. Черчем результаты свидетельствовали, что существуют утверждения, истинность или ложность которых не может быть доказана в рамках данной системы, и что в системе могут быть теоремы, доказательство которых не может быть записано в разумный промежуток времени. Эти выводы были использованы одними математиками для заключения о том, что ТЧК не может быть ни доказана, ни опровергнута, а другими - для заключения о невозможности записать доказательство, даже если оно существует, в разумный период времени.
Часть математиков не теряла надежды найти решение ТЧК. Результаты, полученные А. Кемпе и П. Хивудом в XIX веке, а также Д. Биркгофом и Ф. Франклином в XX веке, послужили тем фундаментом, который позволил Г. Хишу формализовать известные методы доказательства сводимости конфигураций и показать, что, по крайней мере, один из них (прямое обобщение метода, использованного А. Кемпе) представляет собой процедуру, которую может осуществить ЭВМ [10]. Теория сводимых конфигураций, развитая Г. Хишем, к концу 80- годов XX века позволила уяснить необходимые для доказательства ТЧК идеи сводимости. Однако на пути доказательства ТЧК стояли еще два препятствия: недостаточный для доказательства ТЧК объем памяти существующих ЭВМ и неясность того, каков должен быть верхний предел необходимости для доказательства ТЧК сводимых конфигураций. Решающий шаг был сделан К. Аппелем и В. Хакеном.
Вначале К. Аппелем и В. Хакеном было найдено множество сводимых конфигураций, «размер кольца которых был достаточно мал, чтобы машинное время на доказательство сводимости было в пределах разумного» [10, р. 115]. Это позволило к концу 1972 года составить машинную программу для выполнения специального типа разряжающей процедуры. Прогонки этой программы позволили ее модифицировать при сохранении основной структуры. Это позволило на основе новой разряжающей процедуры построить множество сводимых конфигураций, в результате чего в конце 1976 года ТЧК была доказана (на что потребовалось 1200 часов машинного времени трех ЭВМ).
Таким образом, оказалось, что существуют такие математические утверждения, проверка которых требует объема вычислений и затрат времени, превышающих возможности не только отдельного человека, но и большого коллектива. Поэтому использование ЭВМ для решения подобных задач не только возможно, но и необходимо. Известно, что в традиционных доказательствах могут быть опущены некоторые моменты по причине их очевидности. Допускаются также ссылки на работы, в которых можно найти то, что пропущено в доказательстве. В том и другом случае подразумевается, что пропущенное может быть при желании восполнено. Использование же ЭВМ в математическом доказательстве создает ситуацию, в которой такой очевидной возможности нет.