Десять лет назад американский математик Томас Хейлс доказал наконец сформулированную еще в 1611 году гипотезу Кеплера и отправил статью в научный журнал.
Ответ пришел через четыре года. «Рецензенты приложили беспрецедентные усилия», - писал Хейлсу редактор журнала. Они не нашли ни одной ошибки. «Но удостоверить корректность доказательства в целом они не смогли и в будущем тоже не смогут, потому что сил на эту задачу у них больше нет», - заключил редактор. Статья все же вышла. Таким образом, доказательство было принято, но, можно сказать, без гарантии: 265 страниц текста и 40 000 строчек компьютерного кода никто так и не проверил полностью.
В математике такое случается все чаще. «Большая часть “простых” доказательств давно найдена», - объясняет главный программист корпорации Intel Джон Харрисон. Самые впечатляющие достижения последних лет - это чрезвычайно длинные доказательства. Беда не только в размере, но и в сложности: математика становится все более специализированной. «Мы радостно заявляем, что Великая теорема Ферма доказана, - говорит Роберт Хант из Кембриджа. - Но понять ее доказательство во всем мире может горстка людей».
По мнению Ханта, ни в какой другой науке такая ситуация невозможна. Эйнштейну не верили, что лучи света искривляются под воздействием гравитации, пока это не подтвердили эксперименты. Уотсону и Крику не верили, что в клетках всех живых существ есть ДНК, пока с этим не согласилось множество других биологов. А в математике приходится полагаться на мнение нескольких экспертов или, хуже того, как в случае с Хейлсом, фактически только на самого автора.
Харрисон, Хейлс и некоторые другие математики уверены, что эту проблему можно решить - с помощью так называемых формальных доказательств (ФД). Им посвящен декабрьский выпуск журнала Notices of the American Mathematical Society. ФД - это очень подробное доказательство, записанное на формальном языке, который понятен и человеку, и компьютеру. Таким образом, цепочку рассуждений может проверять машина, которая делает это быстро и безошибочно.
У ФД есть и практическое применение. «Мы живем в мире чудовищно сложных технологий, которые нам все труднее контролировать, - говорит Хейлс. - С помощью нового инструмента можно убедиться, что в компьютерных программах нет багов, что компьютерное железо работает правильно и что лежащая в основе всего этого математика безошибочна». Фрейк Видайк из голландского Университета Радбауд в Неймегене считает, что в математике было три революции. Первую совершили древние греки в IV веке до н. э. - они ввели понятие доказательства. Вторая произошла в XIX веке, когда исследователи придали математике необходимую строгость. Третья - введение ФД - идет сейчас.
ЧТО ЕСТЬ ИСТИНА
С доказательствами в математике все не так просто. Даже найти определение понятию «доказательство» - серьезная проблема. Профессор мехмата МГУ Владимир Успенский предлагает формулировку: «Доказательство - это убедительное рассуждение, убеждающее нас настолько, что с его помощью мы способны убедить других». В математике формального определения доказательства нет. «Признание доказательств зависит от того, насколько они убеждают отдельных математиков», - соглашается Джон Харрисон.
Представления об убедительности меняются с ходом истории. Это затрагивает и математику. Успенский приводит три примера: Древний Египет, Древнюю Грецию и средневековую Индию. В Египте - централизованном теократическом государстве с непререкаемым авторитетом фараона и жрецов - непререкаемым авторитетом обладало и любое написанное слово. Написано - значит верно. На египетских папирусах записано, как вычислять площади фигур, но безо всяких обоснований. В маленьких полисах демократической Греции ораторы убеждали сограждан своими речами. Именно в Греции берут начало дисциплины, основанные на рассуждениях, - юриспруденция и математика. А в Индии главным источником знания считалось внутреннее озарение. Чтобы убедить собеседника в истинности теоремы, надо, чтобы он испытал такое озарение. Поэтому индийские доказательства представляли собой чертеж с подписью «Смотри!».
Сейчас идут горячие споры, можно ли считать корректными многие доказательства XVIII–XIX веков. А через несколько столетий, по мнению Фрейка Видайка, математики не будут считать точным то, что не было доказано с помощью ФД.
КОМЕДИЯ ОШИБОК
Как показывает опыт, проверка доказательств действительно необходима. Книга про ошибки крупных математиков, сделанные до 1900 года, насчитывает 130 страниц. «Сейчас бы понадобился том побольше, а то и специальный журнал», - считает Харрисон. «Бывает, доказательство опубликовали, признали, лет 15 прошло, человеку уже и премию какую-нибудь успели дать, а тут вдруг выясняется, что оно неправильное», - подтверждает лауреат премии Филдса (самая известная премия в математике) Владимир Воеводский из принстонского Института передовых исследований.
В 1993 году Эндрю Уайлс объявил, что доказал Великую теорему Ферма, которой, наверное, принадлежит абсолютный рекорд по числу неправильных доказательств. Уайлс быстро понял, что и его доказательство ошибочно. В 1994-м он устранил свою ошибку, и теперь доказательство Уайлса считается правильным, хотя проверили его лишь несколько человек.
«Расплывчатый социальный процесс, которым сейчас является проверка доказательств, выглядит еще более пугающим, если вспомнить, что математика применяется в реальном мире», - говорит Харрисон. То, что самолеты не падают сплошь и рядом, - прямое следствие точного математического расчета. Ученые, правда, затрудняются привести примеры, когда на практике применялась ошибочная математическая теорема. Но некоторые из теорем, которым люди уже нашли практическое применение, не доказаны. «Люди пользуются гипотезами на свой страх и риск», - говорит Хейлс. Так, например, для анализа сложности алгоритмов шифрования и дешифровки используется недоказанная гипотеза Римана.
Даже если предположить, что интуиция подводит математиков нечасто и неверные теоремы никто не использует, ФД все равно имеют огромное прикладное значение. Эти методы применимы не только к математическим теоремам, но и, например, к компьютерным программам. Подсчитано, что готовые программы содержат в среднем одну ошибку на сто строчек кода. Эти ошибки могут обойтись очень дорого. В 1996 году взорвалась ракета «Ариан-5». Компьютерный баг стоил Европейскому космическому агентству $0,5 млрд. А двумя годами раньше корпорация Intel была вынуждена отозвать целую серию своих процессоров. Ошибку, кстати, обнаружил математик. Подобных случаев можно избежать, если компьютерные программы будут проверяться с той же точностью, что и самые надежные из математических доказательств.
МЕХАНИЧЕСКАЯ ПРОВЕРКА
Доказательство - это последовательность утверждений, в которой каждое утверждение вытекает из предыдущего. Это значит, что математику, прочитавшему предыдущее утверждение, должно быть понятно, почему верно и следующее. А вдруг он ошибся? В ФД «вытекает из предыдущего» означает, что утверждение автоматически выводится из предыдущего по строгим правилам, которые понятны машине. А это значит, что ФД могут проверяться не человеком, а компьютером. И компьютер не ошибется: несложную программу проверки ФД легко довести до совершенства вручную.
Каждое утверждение в ФД - это набор символов из алфавита формального языка. Есть ряд правил, которые разрешают заменять определенные последовательности символов на другие. Такие замены позволяют из одного утверждения получать другое. Это можно условно сравнить с умножением чисел в столбик. Заучив формальный алгоритм, любой человек сможет перемножать числа абсолютно правильно, даже если вообще ничего не знает об арифметике. Так и с ФД: любой математик проверит доказательство даже из той области, в которой он не разбирается. Такая проверка - очень долгий и кропотливый механический процесс, но важно, что она в принципе возможна. И главное, доступна компьютерной программе.
От людей требуется создать подходящий формальный язык и программу, которая умеет проверять записанные на нем доказательства. Это непросто, но возможно. Уже есть несколько таких программ. Фрейк Видайк отслеживает, сколько теорем из «100 величайших» (условный список, составленный на рубеже тысячелетий) уже доказаны с помощью ФД. На момент выхода данной статьи - 81: теорема Пифагора, иррациональность корня из двух, бесконечность простых чисел, площадь круга и многие другие. Сотой в очереди стоит Великая теорема Ферма.
Самый трудоемкий процесс - перевести доказательство в формальный вид. Уже подсчитано, что оно в среднем удлиняется в четыре раза, а формализация одной страницы университетского учебника занимает около недели. Ведь ни один шаг нельзя пропустить, ни одно утверждение нельзя объявить очевидным или интуитивно понятным, все нужно записать максимально подробно. В конечном итоге доказательство должно опираться на аксиомы. Это главная причина непопулярности формальных доказательств среди математиков. Многие считают, что перевести основы современной математики в формальный вид не удастся никогда - слишком много труда требует этот нетворческий процесс.
Томаса Хейлса это не пугает. Он так и не смирился с тем, что математическое сообщество не смогло нормально проверить его доказательство гипотезы Кеплера. В 2003 году Хейлс начал записывать свое доказательство на формальном языке. И записывает до сих пор.
Александр Бердичевский
Текст www.runewsweek.ru
Фото www.math.pitt.edu