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

К 1948 г. Тьюб эволюционировал в новую машину, названную Бэби. Ее отличало новшество: она могла на высокой скорости считывать и устанавливать случайные биты информации, сохраняя значение бита между установками. Это был первый компьютер, который мог запоминать произвольную (небольшую) программу в электронном хранилище данных и выполнять ее с электронной скоростью. Килберн и Уильямс продолжали работу над своими идеями, что привело в 1949 г. к созданию Манчестер Марк 1. Это был первый, компьютер, обладавший памятью со случайным доступом (аналогичную памяти, которая используется в современных компьютерах). Она отличается тем, что данные не хранятся в последовательном порядке, как на ленте. Вместо этого они сохраняются таким образом, что могут считываться электронно с высокой скоростью.

В 1944 г. счастливый случай свел Джона фон Неймана (1903–1957) и Германа Голдстина (1913–2004) на железнодорожной станции в Абердине, Мэриленд. Именно тогда фон Нейман узнал о проекте EDVAC (Electronic Discrete Variable Automatic Computer — электронный автоматический компьютер с дискретной переменной) в Пенсильванском университете. Он включился в этот проект и в 1945 г. написал статью, изменившую направление развития компьютерных наук. До тех пор компьютеры (такие как ENIAC) требовалось переконфигурировать для каждой новой задачи. Фон Нейман сообразил, что инструкции для компьютера можно хранить внутри машины, и предложил таким образом новую идею программируемого компьютера — именно такими мы представляем себе компьютеры сегодня. В конце концов фон Нейман и Голдстин вернулись в Принстонский институт высших исследований, штат Нью Джерси, где работали над компьютером, воплощая идеи фон Неймана. Многие считают его (математика по образованию) отцом современного компьютера.

В 1956 г. А. Ньюэлл (1927–1992) и Г. Саймон (1916–2001) разработали программу «машина теории логики», которая могла доказывать теоремы исчисления высказываний (это часть формальной логики, которая имеет дело с соотношениями между высказываниями). На практике машина теории логики могла находить только очень короткие доказательства. Ее очень скоро сменила геометрическая машина Гелернтера. Ограничившись отдельной ветвью математики (геометрией), Гелернтер достиг большей эффективности.

В том же году начался проект по автоматизации доказательств всех результатов из Principia Mathematica Уайтхеда и Расселла с использованием машины теории логики Ньюэлла и Саймона. Этот проект был завершен в 1959 г.

К 1960 г. три технологии доказательств теорем были разработаны П. Гилмором, Г. Вангом (1921–1995) и Д. Правицем (р. 1936). Эти системы справлялись только с самыми элементарными утверждениями и доказательствами.

В конце 1960-х годов одна группа в Applied Logic Corporation из Принстона, штата Нью Джерси, разработала систему SAM (semi-automated mathematics — полуавтоматизированная математика). Ее отличала возможность работать под руководством и вмешательством человека.

В 1967 г. система проверки доказательств Automath была разработана в техническом университете Эйндховена Н. Г. де Брейном и его коллегами. В ней использовался особый язык для записи и проверки математических утверждений.

В 1972 г. Р. А. Овербик создал систему доказательства теорем Aura (Automated Reasoning Assistant — ассистент автоматических рассуждений). Затем ее сменила и превзошла система Otter (Organized Techniques for Theorem-proving and Effective Research — организованные техники доказательства теорем и эффективных исследований). Среди современных мощных систем для математических доказательств следует указать HOL Light (Higher Order Logic — логика высшего порядка), Mizar, ProofPower, Isabelle и Coq. Подробную информацию об этих средствах можно получить в статьях [HAL3] и [WIE].

Перечислим важнейшие достижения в развитии компьютерного доказательства.

• Первая теорема Гёделя о неполноте. Она гласит, что в любой достаточно сложной логической системе (включающей арифметику) существуют истинные утверждения, которые нельзя доказать. Подробнее об этом можно прочитать в разд. 1.11. Шанкар использовал компьютерную утилиту ngthm для построения «формального доказательства» (т. е. компьютерного доказательства, исходящего из самых базовых аксиом и представляющего собой утомительную пошаговую логическую процедуру) этого результата в 1986 г. С этой же целью О’Коннор в 2003 г. воспользовался системой Coq, а Гаррисон в 2005 г. — системой HOL Light.

• Теорема о жордановой кривой. Это теорема о том, что плоская замкнутая кривая без самопересечений делит плоскость на две области — ограниченную и неограниченную. Интуитивно очевидная, эта теорема чрезвычайно сложна для доказательства в традиционном смысле этого слова. В 2005 г. с помощью системы Mizar Томас Хейлс дал формальное доказательство этого факта.