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

Существует и такое интересное мнение, что многие компьютерные доказательства по природе своей слишком длинны и сложны для того, чтобы представлять какую-либо пользу для людей. В 1972 г. Альберт Мейер из MIT показал, что компьютерные доказательства некоторых произвольно выбранных утверждений в очень простой логической системе (с одной только операцией — прибавить единицу к натуральному числу) безнадежно длинны. Позднее было показано, что в той же очень простой логической системе существуют утверждения длиной 617 и менее символов, которые требуют 10¹²³ компонентов. А ведь 10¹²³ — число объектов размером с протон, которые могут плотно заполнить нашу вселенную. Урок в том, что, хотя компьютерные доказательства представляют интерес и продолжают открывать для нас новые истины, они имеют свои ограничения. Непохоже, что когда-нибудь компьютеры станут генерировать все нужные нам доказательства.

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

Есть забавная история, иллюстрирующая это утверждение. В этой книге мы уже говорили о том, что фон Нейман придумал и разработал первый программируемый компьютер в Принстонском институте перспективных исследований. Вместе с ним над проектом работала целая команда сотрудников, и среди них Герман Голдстин.

Джон фон Нейман был выдающимся математиком и очень хорошо считал в уме. Кроме того, у него была фотографическая память: он без усилий воспроизводил длинные пассажи из романов, прочитанных двадцать лет назад. Кроме создания (вместе с Германом Голдстином) одного из первых программируемых компьютеров фон Нейман активно работал как математик и консультант. Он постоянно разъезжал по стране, помогая правительственным агентствам и частному бизнесу, распространяя влияние своей эрудиции. Говорят, что доход от этой деятельности (не считая зарплаты в Принстонском институте) был довольно существенным. Да к тому же фон Нейман был довольно богат благодаря фамильному состоянию.

Во время одной из таких консультационных поездок Герман Гольдстин и другие продолжали работу над новым компьютером, проводя тестирование. Они ввели большое количество результатов метеорологических наблюдений, включили машину на всю ночь и к утру получили очень интересные выводы. В тот же день, только позднее, из поездки вернулся фон Нейман. Собираясь подшутить над ним, коллеги решили не рассказывать ему об успешной работе компьютера, а преподнести все так, словно они получили результаты вручную. За чаем они рассказали фон Нейману, что работали над такой-то задачей с такими-то данными, и на первом шаге получили … «Нет-нет», запротестовал фон Нейман, приложил руку ко лбу, откинулся назад и дал ответ. Точно такой же утром дала и машина. Они продолжали: «На втором же шаге вышло…» «Нет, нет, — опять запротестовал фон Нейман. — Дайте-ка мне подумать». Он опять откинулся назад — теперь это заняло больше времени — и через несколько мгновений дал ответ. И наконец, сотрудники сказали «А вот на третьем шаге…» И опять фон Нейман пожелал посчитать сам. Он откинулся назад и принялся размышлять. Спустя несколько минут он все еще размышлял, так что они раскрыли ответ. Джон фон Нейман вышел из транса и сказал: «Да, совершенно верно. Но как вам удалось сосчитать быстрее меня?»

Про необыкновенное умение фон Неймана считать в уме рассказывают еще одну историю. Она был на вечеринке, и кто-то задал ему головоломку:

Расстояние между двумя поездами составляет 50 миль. Они движутся навстречу друг другу по одному пути со скоростями 25 миль в час. С одного из поездов взлетает муха и со скоростью 40 миль в час летит к другому, а затем немедленно возвращается к первому. Так она и летает туда-сюда, пока поезда ее не раздавят. Сколько всего миль пролетит муха?

Джон фон Нейман выпалил верный ответ — 40 миль. Его друзья сказали: «О, здорово, ты догадался». (Догадаться надо было о том, что поезда встретятся через один час, и за этот час муха как раз 40 миль и пролетит.) Но фон Нейман ответил, что он просто-напросто просуммировал бесконечный ряд.

Забавно и поучительно (и ужасно утомительно) посмотреть, что же это за ряд. Вначале заметим, что если ситуация выглядит так, как на рис. 7.5, когда муха стартует с левого поезда, то мы можем вычислить, когда она впервые долетит до правого, с помощью уравнения