Тёрстон формулирует программу геометризации. 1980
Кнут создает TEX. 1984
Де Бранж доказывает гипотезу Бибербаха. 1984
Шанкар дает автоматизированное доказательство теоремы Гёделя о неполноте. 1986
Паульсон и Нипков создают доказыватель теорем Isabelle. 1988
Гордон создает доказыватель теорем HOL. 1988
Канада и Тамура вычисляют 1 000 000 000 знаков числа π. 1989
Хоффман, Хоффман и Миикс используют компьютер для порождения вложенных минимальных поверхностей. 1990
Трайбулек создает доказыватель теорем Mizar. 1992
Хорган публикует «Смерть доказательства?» 1993
Хсианг публикует «решение» задачи Кеплера. 1993
Эндрю Уайлс доказывает Великую теорему Ферма. 1994
Проводится классификация конечных простых групп. 1994
МакКьюн создает программное обеспечение для доказательства теорем Otter. 1994
МакКьюн с его помощью доказывает гипотезу Роббинса. 1997
Альмгрен пишет 1728-страничную статью по регулярности. 1997
Хсианг публикует книгу с «решающим» доказательством задачи Кеплера. 2001
Канада, Уширо и Курода вычисляют 1 000 000 000 000 знаков числа π. 2002
Перельман объявляет о доказательстве гипотезы Пуанкаре. 2004
Хейлс и Фергюсон представляют компьютерное решение задачи Кеплера. 2006
Из этого интеллектуального окружения выросла основополагающая работа Фреге об основаниях математики (позднее мы обсудим ее подробно). Еще одна веха в математической мысли той поры — «Principia Mathematica» [WRU] Расселла и Уайтхеда. Бертран Расселл, которому тогда еще только предстояло стать выдающимся философом, был студентом старшего коллеги Альфреда Норта Уайтхеда в Кембриджском университете. Они поставили задачу, пользуясь только логикой, вывести всю математику из минимального набора аксиом. Смысл в том, чтобы пользоваться только строгими правилами логического вывода и не употреблять никаких слов! Только символы! В результате получился массивный трехтомный труд, оказавшийся практически нечитаемым. Это было упражнение в чистой математической логике, доведенное до последней крайности. Например, после 1200 страниц упорного труда была получена теорема 2+2=4.
В своей автобиографии Расселл признался, что он «никогда вполне не избавился от напряжения», потребовавшегося для написания этого монументального труда. После того как он был закончен, Расселл прекратил занятия математикой и стал чистым философом.
В наше время есть не так много людей — даже среди математиков, — которые изучают книгу Уайтхеда и Расселла. Но она стала важным шагом в развитии математической строгости, в понимании того, каким должно быть доказательство. Сейчас создано программное обеспечение, такое как Isabelle, которое на входе получает математическое доказательство (в таком виде, как современные математики используют в публикуемых статьях) и переводит его в формальное доказательство, в духе Уайтхеда и Расселла или аксиом теории множеств Цермело—Френкеля.
Наверное, надо подчеркнуть, что Уайтхед и Расселл стремились дать строго формальное построение математики. Их цель была вовсе не в том, чтобы создать что-то читаемое или понятное или хотя бы обучающее[23]. Они поставили цель создать архив математики, пользуясь правилами формальной логики. Сегодня математическая статья, написанная в духе Уайтхеда и Расселла, не будет опубликована. Ни один журнал не станет ее рассматривать, ведь такой способ выражения никак нельзя отнести к эффективной математической коммуникации.
Математические доказательства, как мы их публикуем сегодня, конечно же, менее формальны, чем в модели Уайтхеда—Расселла. Хотя мы и привержены строгим правилам рассуждения, некоторые шаги мы опускаем, иногда мы немного перескакиваем и оставляем подробности читателю, потому что хотим передавать свои идеи наиболее эффективным и изящным способом. Обычно публикация представляет собой набор орудий, с помощью которых читатель может самостоятельно построить свое собственное доказательство.
Примерно так же действуют химики: публикуют статью с описанием того, как проводился некоторый эксперимент (и какие выводы можно сделать), так что заинтересованный читатель может такой эксперимент воспроизвести. Часто бывает так, что важная химическая статья, описывающая годы напряженной работы десятков человек, содержит всего лишь несколько страниц. Это крайнее применение бритвы Оккама: записываются только ключевые идеи, так что другие ученые при необходимости могут воспроизвести эксперимент.
1.8 Платонизм или кантианство
23
На самом деле — и это представляется поразительным, если учесть, сколь важна их работа — им с трудом удалось опубликовать «Principia Mathematica». Им даже пришлось взять часть расходов по публикации на себя!