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