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

Платон в «Республике» обсуждает понятие доказательства. ~380 до н. э. 

Евдокс развивает понятие теоремы. ~368 до н. э.

Аристотель обрисовывает методы доказательства (в «Физике»). ~330 до н. э.

Евклид пишет «Элементы». ~285 до н. э.

Эратосфен изобретает решето. ~236 до н. э.

В Индии мыслители разрабатывают полную схему десятичной арифметики (включая 0). ~450

Аль-Хорезми создает алгебру. ~820

Кеплер формулирует свою гипотезу об упаковке сфер. 1611

Ферма закладывает основы дифференциального исчисления. 1637

Исаак Ньютон и Готфрид Лейбниц создают анализ. 1666

Ламберт доказывает иррациональность числа π. 1770

Гаусс доказывает основную теорему алгебры. 1801

Фурье публикует свой труд «Аналитическая теория тепла». 1822

Абель доказывает неразрешимость уравнения пятой степени. 1824

Галуа записывает идеи теории Галуа (включая группы). 1832 

Бэббидж разрабатывает аналитическую машину. 1833

Риман формулирует гипотезу Римана. 1859

Джевонс конструирует логическое пианино. 1869

Кантор публикует свои идеи о кардинальности и бесконечности. 1873

Линдеманн доказывает трансцендентность числа π. 1882 

Адамар и де ла Валле Пуссен доказывают теорему о простых числах. 1896

Гильберт публикует «Основания геометрии». 1899

Гильберт читает лекцию с 23 проблемами. 1900

Ден решает третью проблему Гильберта. 1900

Создается парадокс Расселла. 1902

Фреге публикует «Основания арифметики». 1903

Пуанкаре формулирует свою гипотезу о сферах. 1904

Брауэр основывает движение интуиционистов. 1908

Уайтхед и Расселл пишут Principia Mathematica. 1910

Создается корпорация International Business Machines (IBM). 1911

Разрешается парадокс Банаха—Тарского. 1924

Гёдель публикует теорему о неполноте. 1931

Выходит из печати первая книга Бурбаки. 1939

Эрдёш и Сельберг дают элементарное доказательство теоремы о простых числах. 1949

Фон Нейман и Голдстин создают программируемый компьютер. 1952

Ньюэлл и Саймон разрабатывают Logic Theory Machine. 1955

Гелернтер создает геометрическую машину. 1959

Гилмор, Ванг и Правиц создают машину, доказывающую теоремы. 1960

Работает доказыватель теорем SAM V. 1966

Робинсон изобретает нестандартный анализ. 1966

Бишоп публикует «Основания конструктивного анализа». 1967

Де Брейн изобретает систему проверки доказательств Automath. 1967

Кук вводит NP-полноту. 1971

Овербик создает доказыватель теорем Aura. 1972

Гиллауд и Буйер вычисляют 1 000 000 знаков числа π . 1973

Аппель и Хакен дают компьютерное доказательство теоремы о четырех красках. 1976

Джобс и Возняк создают персональный компьютер для массового потребителя. 1977

Тёрстон формулирует программу геометризации. 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.

В своей автобиографии Расселл признался, что он «никогда вполне не избавился от напряжения», потребовавшегося для написания этого монументального труда. После того как он был закончен, Расселл прекратил занятия математикой и стал чистым философом.