Инженер для получения нужных результатов может пользоваться математикой эвристически. Физик для достижения своих целей может использовать аппроксимацию. Те люди, которые математикой пользуются, вообще говоря, не доказывают теорем[22]. Но они пользуются математическими идеями. И они знают, что могут полагаться на математику в силу ее внутренней непротиворечивости.
В табл. 1 мы представляем ленту времени, включающую основные события в истории математического доказательства. Все эти события в нашей книге рассматриваются.
1.7 Логические основания математики
В конце XIX века связи между математиками разных стран заметно выросли. Отчасти благодаря этой новой открытой культуре общения появилось осознание того, что математика очень разрознена и фрагментирована. В идеале математика должна быть изначально единым логическим построением. Она вся должна вытекать из одного набора определений и одного набора аксиом. По крайней мере, именно об этом мечтал Давид Гильберт (гл. 5, особенно разд. 5.1).
Вавилонская табличка с первым доказательством. ~1800 до н. э.
Фалес использует доказательства. ~600 до н. э.
Пифагор доказывает, что число 
иррационально. ~529 до н. э.
Протагор дает некоторые из первых формальных доказательств. ~430 до н. э.
Гиппократ изобретает доказательство от противного. ~420 до н. э.
Платон в «Республике» обсуждает понятие доказательства. ~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
22
Бывают и исключения. В инженерном журнале IEEE Transactions in Signal Processing часто публикуются статьи с математическими доказательствами. Там недавно отклонили статью одного моего друга из-за пробелов в доказательстве.