Когда-то считалось, что математическое доказательство должно быть кратким, простым и понятным человеку. Сейчас представление о таком идеальном доказательстве уходит в прошлое. Так в 1976 г. В. Хакен и К. Аппель сообщили о компьютерной программе, которая проанализировала 1482 графа, представляющие все возможные конфигурации на географической карте. При этом было доказано, что любую карту можно раскрасить четырьмя цветами так, чтобы никакие две соседние области не были одного и того же цвета.
Хотя вычисления проводились более 1000 часов, результаты все же можно было (теоретически) проверить от руки. Но вот в конце ноября 1988 года появилась публикация о решении другой задачи, которая раз и навсегда покончила с самой идеей ручной проверки. После вычислений, продолжавшихся около 3000 часов на супер-компьютере CRAY-l (вычисления выполнялись более двух лет в кратчайшие свободные промежутки времени в процессе решения других задач), К. Лэм из Университета Конкордия в Монреале объявил, что руководимая им группа математиков и программистов-исследователей доказала справедливость одного из частных случаев предположения, впервые высказанного Карлом Фридрихом Гауссом почти 200 лет назад.
Их результат, заключающийся в том, что не существует конечных проективных плоскостей 10-го порядка, проверить практически невозможно. (Такую конечную проективную плоскость, если бы она существовала, можно представить в виде матрицы из 111 строк и столбцов, причем в каждой строке было бы заполнено ровно 11 позиций, и любые две строки имели бы единственную общую заполненную позицию.) Чтобы доказать, что таких плоскостей действительно не существует, компьютер CRAY за два года проанализировал около 100 триллионов различных вариантов.
Более того, отмечает Дж. Маккей, один из коллег Лэма, результат был получен не одной программой, а набором небольших программных «фрагментов», каждый из которых предназначался для обработки какой-либо одной грани задачи. «Я надеялся на положительный результат, потому что его можно было бы проверить» говорит Лэм. Но вместо этого он столкнулся с уймой отрицательных результатов, каждый из которых мог быть и ошибочным.
И все же, Лэм доверяет своему результату, а математики, похоже, доверяют Лэму. Отчасти это доверие, как говорит Лэм, объясняется тем, что программы содержали внутренние проверки, благодаря которым простые ошибки вычислений можно было легко обнаружить. Математическая интуиция также говорит в пользу Лэма. Так, ранее уже было доказано, что проективная плоскость 10-го порядка, если бы она существовала, не должна иметь симметрии, а это звучит совершенно невероятно по отношению к такому сложному объекту.