Теория множеств — это один из подходов к построению основы для математики. Другой подход находится сейчас в процессе формирования и подразумевает использование компьютеров. Система для проверки доказательств — это элемент программного обеспечения, проверяющий правильность логических выводов, имеющихся в доказательстве[173]. Хотелось бы верить, что когда-нибудь компьютеры смогут доказать любое математическое утверждение[174]. Если вы захотите убедиться в том, что теорема верна, вам будет достаточно просто нажать кнопку.
Первой крупной теоремой, доказанной с помощью компьютера, стала теорема о четырехцветной карте, или теорема о четырех красках. Мы с вами уже удостоверились, что любой машинальный рисунок может быть двухцветным, другими словами, что мы можем заштриховать его фрагменты так, чтобы две смежные области всегда были разных цветов. В 1852 году проживающий в Лондоне выходец из Южной Африки Френсис Гатри раскрашивал карту графств Англии. Он обнаружил, что для раскраски карты таким образом, чтобы соседние графства имели разные цвета, достаточно четырех красок. Эксперименты показали, что четырех цветов хватает и для того, чтобы раскрасить так любую карту. Однако больше столетия никто не мог это доказать, пока в 1976 году Кеннет Аппел и Вольфганг Хакен из Иллинойского университета не сделали это, воспользовавшись суперкомпьютером для проверки всех вероятных конфигураций карт. Математики отреагировали неоднозначно[175]. В принципе должна существовать возможность проверить каждую строку доказательства. Но компьютер выполнил слишком большой объем вычислений, для того чтобы можно было их все проверить, а это противоречило эталону доказательства теорем, использовавшемуся со времен Евклида. Однако помимо сугубо философских возражений против такого метода доказательства теорем существовали и другие претензии практического плана. В программах всегда есть ошибки. Разве могли Аппел и Хакен быть полностью уверены в том, что в их программе их нет? Нет, не могли. На самом деле в их доказательстве до сих пор находят новые компьютерные ошибки, хотя все обнаруженные ошибки были исправлены. В 1995 году группа исследователей Принстонского университета составила усовершенствованное компьютерное доказательство теоремы о четырехцветной карте. А в 2004 году Джордж Гонтье из исследовательской лаборатории компании Microsoft в Кембридже (Англия) проверил его с помощью специальной программы, определяющей корректность доказательств, хотя для этого ему пришлось перевести все концепции на специальный язык программирования, который понимала эта программа. Но тогда возникает следующий вопрос: разве можно быть уверенным в том, что такая программа-помощник не содержит ошибок? Нет, полной уверенности в этом нет, однако ее уровень все же выше, чем в случае исходных доказательств, поскольку эта программа была многократно протестирована при выполнении многих других задач. В настоящее время доказательство теоремы о четырех красках — одно из наиболее тщательно проверенных в математике.