Многие математики исходят из того, что доказательство должно обладать такими характеристиками, как убедительность, обозримость и формальность. Убедительность доказательства - это свидетельство понимания математики как человеческой деятельности. Обозримость - свидетельство возможности проверить (обозреть) его во всей полноте человеком, т.е. обозримость конкретизирует убедительность, связывая процесс доказательства с его субъектом. Традиционно источником убедительности доказательства считается ясность, т.е. возможность проверить его квалифицированным математиком без использования ЭВМ, хотя некоторые доказательства могут быть весьма длинными, и потребовать много сил и времени. Формальность доказательства означает представимость его в виде конечной последовательности формальной теории, удовлетворяющей некоторым условиям, т.е. это вывод заключения из аксиом теории с помощью правил логики. Формализованное^ доказательства, в свою очередь, конкретизирует обозримость, разбивая ее на конечные обозримые модели.
Когда в доказательстве присутствуют обозримость и формальность, это решающий аргумент в пользу признания доказательства математиками. Большинство их полагает, что все обозримые доказательства могут быть формализованными, хотя интуиционисты отрицают возможность замены актуальных конструкций математических доказательств формальными системами. Кроме того, теорема Геделя свидетельствует о том, что ни одна теория не в состоянии формализовать каждое доказательство. В таком случае ясно, что обозримое доказательство можно формализовать в более сильной формальной теории, но в последней будут содержаться новые обозримые доказательства, которые в ее рамках не могут быть формализованы.
Таким образом, не существует системы, в которой любое доказательство может быть формализовано, поэтому формализованность называют локальной характеристикой доказательств, а не глобальной. Но, как было показано Р. Томом, для любого доказательства существует некоторая подходящая формальная система, в которой оно может быть формализовано [11]. Однако все ли формализованные системы обозримы? Существуют формализованные доказательства, которые не могут быть обозримы вследствие ограниченности человеческой жизни. Поэтому возможны формализованные утверждения без обозримого доказательства. На практике же математики обычно приходят к знанию формального доказательства через посредство обозримых доказательств. Убедительность и обозримость могут быть связаны как сопряжения целого и части. Если убедительность - это в известной мере осуществимость доказательства как целого, завершенного, но в котором особо выделены исходный и заключающий его пункты, то обозримость - это осуществимость доказательства в каждом пункте сцепления доказательства. Формализованность же - упрощающая процедура, делающая доказательство более лаконичным и универсально выраженным, а также делающая его доступным для задания ЭВМ.
В какой же мере указанные характеристики применимы к доказательству ТЧК с помощью ЭВМ? Прежде всего, является ли оно убедительным? К. Аппель и В. Хакен подметили любопытную особенность, заключающуюся в том, что признание убедительности доказательства ТЧК с помощью ЭВМ зависит от характера полученного математического образования: математики, получившие образование до появления ЭВМ, к признанию убедительности данного доказательства относятся, как правило, оппозиционно [10].
Является ли доказательство ТЧК обозримым? Отрицание возможности обозримости основывается на том, что ни один математик не в состоянии проверить его шаг за шагом. По мнению некоторых исследователей, доказательство ТЧК может быть признано обозримым лишь в том случае, если применение ЭВМ считать новым методом доказательства. Но тогда само понятие доказательства должно измениться [11]. Отсюда делается вывод, что обозримость сохраняется за традиционным доказательством, но не доказательством с помощью ЭВМ.
Наконец, является ли доказательство ТЧК формализованным. Оно убедительно, формализовано, но необозримо. Существенное различие между доказательством ТЧК и традиционным заключается в том, что первое требует обращения к ЭВМ для заполнения бреши в доказательстве, которое в остальных отношениях традиционно [11]. Иными словами, доказательство ТЧК осуществлено на основаниях, часто являющихся эмпирическими. Поэтому применение ЭВМ в математике вводит эмпирические эксперименты в математику. Доказательство с помощью ЭВМ не является традиционным, т.е. это не априорный вывод утверждения из посылок, поскольку используются данные эксперимента. А это делает доказательство ТЧК первым доказательством a posteriori, что снова поднимает проблему отличия математики от естественных наук.