Изменчивая природа математического доказательства. Доказать нельзя поверить

• Теорема о простых числах. Это знаменитый результат Вале Пуссена и Адамара о распределении простых чисел. У него сложное доказательство, опирающееся на комплексный анализ. Формальное доказательство в 2008 г. построил Джон Харрисон с помощью системы HOL Light.

• Теорема о четырех красках. Мы довольно подробно обсуждали эту терему в гл. 6. Впервые ее доказали Аппель и Хакен с помощью компьютера, производившего миллионы операций. Формальное доказательство в 2004 г. построил Джордж Гонтье, используя систему Coq. Подробнее об этом можно прочитать в статье [GON].

Следует понимать, что компьютерное построение формального доказательства может быть довольно утомительной и сложной процедурой. Например, A. Маттиас подсчитал, что для строго определения числа 1 в терминах логики требуется более 4 триллионов символов. Только представьте себе, сколько усилий нужно, чтобы полностью формализовать доказательство сложного математического факта вроде одного из тех четырех, которые мы только что перечислили!

Интересное ответвление современной истории вычислений — суперкомпьютер. Его крестным отцом можно считать Сеймура Крэя (1925–1996). Он полагал, что суперкомпьютеры должны быть основаны на понятии «параллельные вычисления». Идея в том, что каждый компьютер содержит центральный процессор (CPU). Это чип, в котором проходят все вычисления — манипуляции с нулями и единицами. У суперкомпьютера должно быть несколько CPU — возможно, более 100[83], — и между ними распределяются различные вычислительные задачи. Кроме того, каждый CPU должен иметь свою память, достигающую нескольких гигабайт.

Таким образом одновременно можно проводить много различных вычислений; поэтому конечный результат достигается быстрее. На заре суперкомпьютеров пользователь должен был владеть специальным языком программирования, в котором имелись подпрограммы для разделения труда между различными процессорами. В современных суперкомпьютерах разделение производится автоматически, при этом распределяется стандартный код, который вводит пользователь. Существуют версии языков Fortran, C и C++, которые можно использовать в суперкомпьютерах. Кроме того, для суперкомпьютеров широко распространены такие программные среды, как Message Passing Interface (MPI), OpenMP, Co-Array Fortran и Universal Parallel C.

Много лет самые быстрые машины с параллельной обработкой создавались компанией Сеймура Крэя Cray Research, расположенной неподалеку от Миннеаполиса. Она дала начало многим другим современным высокотехнологичным компаниям. Довольно долго скорость Крэя была эталоном для компьютерного мира. Вот один простой пример: о появлении первого чипа пентиума говорили так: «Теперь Cray I помещается на одном чипе». Этот чип работает со скоростью 100 megaflop/s (или 100 Mflop/s)[84].

Сеймур Крэй был человеком особенным, даже загадочным. Когда он сталкивался с глубокой и сложной задачей, он спускался под землю. Буквально. Много лет Крэй копал штыковой лопатой туннель размером 4 фута × 8 футов, который должен был соединить его дом в Chippewa Falls с озером неподалеку. Крэй говорил, что его лучшие идеи всегда посещали его во время копания: «Когда я рою туннель, часто ко мне приходят эльфы, принося решения моей задачи». Он умер в автомобильной аварии, так и не завершив туннель.

Сегодня с распространением персонального компьютера компьютеризация стала важной частью жизни каждого из нас. Стив Джобс (1955–2011) и Стив Возняк (р. 1950) изобрели персональный компьютер для массового рынка в 1977 г[85].

Компания IBM революционизировала индустрию персональных компьютеров в 1981 г., выпустив первый PC. В этой машине использовалась операционная система, которая была разработана под названием 86-DOS Тимом Патерсоном[86] из Seattle Computer Company. Билл Гейтс из Microsoft купил 86-DOS за $50 000 и превратил ее в MS-DOS, которая служила операционной системой для IBM PC с 1981 по 1995 г.

В 1994 г. У. У. МакКьюн разработал современное сложное программное обеспечение для доказательства теорем — Otter. Otter использовался не только для «переоткрытия» уже известных доказательств, но и для открытия совершенно новых математических теорем и их доказательства. Теперь Otter превзойден новой системой — Prover 9.

7.2 В чем разница между математикой и компьютерными дисциплинами

Когда среднестатистический человек знакомится с математиком, то часто представляет себе, что тот работает за компьютером днями напролет. Такое представление одновременно и верно, и ложно.