Математикам приходится использовать компьютеры там, где они традиционно пользовались только своей головой — в доказательствах теорем. Должны ли ученые довериться машинам?
Игра судоку — головоломка, представляющая собой квадрат 9 на 9 клеток, разбитый на одинаковые блоки 3 на 3 клетки. Задача игрока — расставить в клетках квадрата цифры от 1 до 9 таким образом, чтобы они не повторялись ни в одной строке квадрата, ни в одном его столбце и ни в одном блоке 3 на 3 клетки.
Для упрощения задачи некоторые цифры помещены в квадрат заранее. Расставляя остальные цифры, можно столкнуться с тем, что у головоломки больше одного решения. Возникает вопрос: какое минимальное число цифр-подсказок должно быть в квадрате, чтобы решение головоломки было наверняка единственным?
Как удалось установить группе ирландских математиков в конце 2011 года, таких подсказок должно быть не меньше 17. Для того чтобы доказать это, был разработан специальный алгоритм, позволивший сократить перебор вариантов до 5,5 миллиарда (общее число решений судоку размером 9 на 9 клеток — около 6,7 × 1021, число интересных для задачи вариантов ненамного меньше). Алгоритм был запрограммирован, и после двухлетнего тестирования программа, запущенная на суперкомпьютере, осуществила необходимый перебор.
Сам по себе этот результат, хотя и достаточно красив, не представляет особого интереса ни для любителей головоломок, ни для математиков за пределами узкого круга специалистов. Но применение компьютерного перебора в доказательстве дает повод для дискуссии, выходящей за рамки головоломки судоку.
Можно ли использовать компьютер в математическом доказательстве или, вернее, можно ли считать доказательство, использующее машинные расчеты, строгим — предмет жарких споров, которые начались около 40 лет назад и продолжаются до сих пор.
Любое математическое доказательство может быть записано в виде цепочки абсолютно формальных логических переходов, по строгим правилам связывающих утверждение теоремы с аксиомами (утверждениями, истинность которых принята по умолчанию). Подобная последовательность действий, записанная специальным языком, конечно, доступна для компьютерного анализа. Но вряд ли возможно придумать алгоритм, способный такую цепочку синтезировать. Творческий процесс математического исследования требует озарения, которое позволяет заметить неочевидные связи, перевести задачу на язык других математических объектов, использовать идеи, изначально чужеродные непосредственному предмету интереса. Этот процесс, как и любой процесс познания, лежит за пределами логики, хотя производит абсолютно логичный продукт.
Использование компьютера может быть полезно в тех случаях, когда на определенном этапе доказательства проблема сводится к необходимости сложного, но конкретного технического расчета или, что чаще, к перебору огромного количества вариантов. Такой перебор, производимый вручную, мог бы занять у одного человека многие годы, а компьютер способен сделать его за несколько секунд, часов или дней, в зависимости от мощности процессора, размера оперативной памяти и сложности задачи.
Казалось бы, применение машинного расчета в таких ситуациях не имеет никаких недостатков, наоборот — сплошные достоинства: силы ученых экономятся для творчества, кроме того, исключен человеческий фактор, а значит, вероятность ошибки меньше.
В действительности, доказательства, использующие компьютер, до сих пор не до конца признаются математическим сообществом и считаются чем-то выходящим за рамки «чистой» математики. А 36 лет назад, когда компьютер впервые применили для решения классической задачи, этот факт был принят в штыки абсолютным большинством математиков.
Четыре краски
Первая крупная математическая теорема, доказанная с помощью компьютера, — теорема о четырех красках.
Ее формулировка элементарна и изящна: для того чтобы раскрасить географическую карту так, чтобы никакие два граничащих региона не были одного цвета, достаточно всего четырех разных красок. Подразумевается, что регион — это некая область, очерченная одной замкнутой линией, то есть анклавы (как Калиниградская область в России или Аляска в США) не допускаются. Два региона считаются граничащими, если они имеют протяженную границу, то есть состоящую больше чем из одной точки.
Утверждение, что четырех красок достаточно для раскраски любой карты, было впервые сформулировано в 1852 году южноафриканским математиком и ботаником Фрэнсисом Гутри. Раскрашивая карту английских графств, он заметил, что для работы ему достаточно использовать краски всего четырех цветов. Фрэнсис рассказал о своем наблюдении в письме брату Фредерику, изучавшему математику в Лондоне. Фредерик обратился к своему профессору, известному шотландскому математику Огастесу де Моргану, благодаря которому задача о четырех красках стала известна математической общественности.
Простота формулировки давала повод предполагать, что для теоремы о четырех красках существует либо элементарное доказательство, либо контрпример, то есть пример карты, для раскраски которой требуется по меньшей мере пять цветов. За теорему о четырех красках брались многие математики, но всякий раз безуспешно. Существует легенда, что однажды известный немецкий геометр Герман Минковский, читая лекцию по топологии, неожиданно заявил слушателям: «Теорема о четырех красках все еще не доказана только потому, что до этого ею занимались третьесортные математики. Не сомневаюсь, мне удастся ее доказать». Минковский приступил к доказательству прямо у доски, но не смог завершить его ни на этой лекции, ни на следующей. Несколько недель спустя во время очередного занятия Минковский удрученно заметил: «Небеса разгневаны моим высокомерием. Мое доказательство неверно» — и продолжил читать лекцию с того самого места, на котором прервался, сделав свое смелое утверждение. Возможно, эта история не более чем апокриф, но она отражает суть: на протяжении столетия время от времени появлялись решения проблемы четырех красок, в которых каждый раз достаточно быстро находились ошибки. Нечто похожее происходило со знаменитой великой теоремой Ферма, которая, впрочем, не поддавалась решению еще дольше — более 350 лет.
Только в 1976 году Кеннет Аппель и Вольфганг Хакен из Иллинойсского университета представили доказательство проблемы четырех красок, не содержавшее явных ошибок. Им удалось свести задачу к раскраске 1936 определенных карт. Эта раскраска была произведена на компьютере IBM 386 c 64 килобайтами оперативной памяти, который в остальное время использовался на математическом факультете университета в основном для административных надобностей, не связанных с наукой. Расчет занял более 1200 часов машинного времени, а на все доказательство ушло в обшей сложности около четырех лет. Хотя многие информационные агентства немедленно сообщили, что знаменитая задача наконец решена, а Иллинойсский университет даже поспешил выпустить приуроченную к этому событию почтовую марку, доказательство Аппеля и Хакена было принято в математической среде далеко не однозначно.
Согласно традиции теорема считается доказанной, если ее доказательство прочитано другими учеными, которые скрупулезно, шаг за шагом проверили каждый его логический переход. Чаще всего в роли таких проверяющих выступают рецензенты научных журналов (обычно это лучшие специалисты в соответствующих областях), вычитывающие статьи перед их публикацией и отвечающие за их корректность своей репутацией и репутацией журнала. В особых случаях, как это было с уже упомянутой великой теоремой Ферма, для проверки доказательства созываются целые конгрессы, которые на протяжении нескольких недель заслушивают автора доказательства, стараясь совместно найти в его выкладках возможные изъяны. Ясно, что в случае доказательства Аппеля и Хакена такая проверка была невозможна. Никто не мог поручиться, что в работе компьютера не произошел незначительный сбой, который привел бы к ошибке в раскраске всего одной из почти 2000 карт.
Доказательство Аппеля и Хакена, помимо компьютерных расчетов, включало в себя письменные выкладки невообразимого объема — более 400 страниц вычислений, которые также требовали проверки. В начале 1980-х нашелся смельчак, взявшийся произвести эту проверку, надеясь, что она будет засчитана в качестве дипломной работы в университете. Он прочитал около 20% доказательства и сделал заявление, что в нем есть существенный недочет. В ответ в 1989 году Аппель и Хакен опубликовали полное подробное доказательство со всеми возможными подробностями, в котором никому ошибок найти не удалось, хотя вряд ли хоть кто-то действительно смог дочитать до конца этот труд, состоявший из нескольких сотен страниц сложнейших расчетов.
На сегодняшний день доказательство теоремы о четырех красках удалось избавить от сложных ручных расчетов и свести к компьютерной проверке всего-навсего 633 карт.
Доказательство теоремы о четырех красках — прецедент использования компьютера при решении классических математических задач. В то же время оно примечательно своей длиной и сложностью. Даже после применения компьютера, позволившего значительно сократить вычисления, текст доказательства элементарно формулируемого утверждения имеет астрономическую длину. Проверка классической, «некомпьютерной» его части доступна, помимо авторов, только ограниченому кругу узких специалистов, да и то требует невообразимо много времени, фактически нескольких лет усердной работы. Появление все более длинных и сложных доказательств — достаточно серьезная проблема современной математики. Доказательства в несколько тысяч страниц точно так же плохо поддаются проверке рецензентов научных журналов, как и электронные вычисления.
Чемодан с шариками
Очень похожая ситуация сложилась с другой знаменитой классической задачей — задачей об упаковке шаров.
Представьте, что у вас есть много одинаковых твердых шаров, например бильярдных. Как лучше всего расположить их, чтобы они занимали пространство наиболее плотным образом, то есть чтобы относительный объем зазоров — пустот между шарами — был минимален? Немного поэкспериментировав, легко предположить, что самым плотным расположением является самое естественное: первый слой нужно положить так же, как бильярдные шары лежат на столе в начале партии, то есть когда каждые три ближайших шара лежат в вершинах правильного треугольника. Шары второго слоя нужно класть в углубления, образованные в центрах троек шаров предыдущего уровня. Последующие шары располагаются аналогично: примерно так на рыночных прилавках часто выкладывают яблоки или апельсины. Это расположение шаров называется гранецентрированной кубической упаковкой.
На первый взгляд оптимальность такой упаковки кажется вполне очевидной — сложить шарики более компактно не получается. Можно подсчитать, что относительный объем пространства, который занимают описанным образом расположенные шары, составляет примерно 74%. Гипотезу о том, что плотнее упаковать шары невозможно, выдвинул еще в 1611 году Иоганн Кеплер, первооткрыватель законов движения тел Солнечной системы. А доказательство гипотезы, использующее сложнейшие компьютерные вычисления, появилось только 387 лет спустя, в 1998 году. То есть для решения этой задачи человечеству потребовалось даже больше времени, чем для доказательства теоремы Ферма!
Задача о плотной упаковке шаров, или гипотеза Кеплера, является частью 18-й проблемы Гильберта — одной из 23 кардинальных математических проблем, которые великий немецкий математик Давид Гильберт сформулировал на II Математическом конгрессе в Париже в 1900 году. В своей речи Гильберт сделал попытку наметить основные направления развития математики в XX веке. И решение любой из сформулированных им на конгрессе проблем (некоторые из них не решены до сих пор) стало целью устремлений многих крупнейших математиков мира. Естественно, тот факт, что задача об упаковке шаров была упомянута в этом знаменательном списке, еще больше подогрел интерес математического сообщества к ней. И, как и в случае с теоремой о четырех красках, на протяжении большей части XX века многие ученые усердно бились над ее решением — не только ради науки, но и из тщеславия.
В 1958 году Клоду Роджерсу из Бирмингемского университета удалось доказать, что никакая упаковка не может иметь плотность большую, чем 0,7796 (что примерно на 0,04 больше, чем плотность гранецентрированной кубической упаковки). Другими словами, как бы плотно мы ни складывали шарики в очень большой чемодан, не менее 22% его объема будет занято воздухом.
Уже тогда никто не сомневался, что естественная упаковка с плотностью 0,74048 является оптимальной, то есть в даже наилучшим образом забитом шариками гигантском чемодане чуть более четверти объема — пустое пространство. Сам Роджерс писал: «Многие математики верят, а все физики знают, что плотность (оптимальной упаковки. — Прим. ред.) не превосходит 0.74048», но за следующие 40 лет сделать хоть сколько-нибудь значительный шаг от веры к знанию математикам не удалось.
И вот в 1998 году американец Том Хейлз из Мичиганского университета объявил, что, основываясь на подходе, предложенном еще в 40-е годы венгром Ласло Тотом, и используя весьма сложные компьютерные вычисления, ему удалось окончательно разобраться с гипотезой Кеплера и доказать, что гранецентрированная кубическая упаковка является оптимальной. Доказательство, поданное Хейлзом для публикации в авторитетном журнале «Анналы математики», включало 250 страниц записей и около 3 гигабайт компьютерного кода. Для того чтобы осуществить проверку работы Хейлза, журнал созвал комиссию из 20 лучших специалистов в этой области. Комиссия продолжала свою работу до 2004 года (шесть лет!), лишившись за это время большей части своих членов. В итоге было принято решение опубликовать в журнале теоретическую часть работы, а проверку компьютерной части отложить до лучших времен. На сегодняшний день большая часть алгоритмов Хейлза проверена и задача об упаковке шаров считается «решенной на 99%».
В отличие от теоремы о четырех красках, которая никакого практического значения не имеет (картографы не настолько экономны), задача об упаковке шаров имеет определенные приложения в кристаллографии и криптографии. И все же для реального применения факта об оптимальности гранецентрированной кубической упаковки шаров вполне было достаточно того, что «все физики это знают». Необходимость строгого доказательства утверждений — традиция и основа математики как науки. Проблема в том, что само понятие «строгое доказательство», которое оставалось неизменным с античных времен и до начала XX века, стало постепенно терять смысл.
Кризис традиции
Математики, слушавшие выступление Давида Гильберта в августе 1900 года, отнеслись бы к формулировке «теорема доказана на 99%» с недоумением, если не с презрением.
Для математики того времени — периода расцвета — понятия истинности и строгого доказательства являлись священными коровами. Основополагающим философским взглядом на математику было платоновское представление, что мир математических объектов реален: математики не выдумывают новые теоремы, а как бы открывают их — как Колумб Америку. Было принято считать, что каждое утверждение, сформулированное на математическом языке, является либо ложным, либо истинным, а значит, рано или поздно будет либо опровергнуто, либо строго доказано, то есть связано с аксиомами доступной для понимания всех математиков цепочкой логических переходов.
Вторая в списке сформулированных Давидом Гильбертом основополагающих проблем касалась непротиворечивости аксиом арифметики.
Гильберт видел необходимость, наконец, формально удостовериться, что цепочки логических выводов, которые можно сделать, основываясь на самых базовых математических аксиомах, не могут привести к парадоксальному утверждению, формально являющемуся истинным и ложным одновременно.
Скорее всего, на фоне научного оптимизма, присущего математике конца XIX века, Гильберт и абсолютное большинство современных ему математиков не сомневались в том, что основа основ математики — аксиомы арифметики — непротиворечивы. Оставалось найти доказательство.
Но произошло неожиданное. Через 30 лет после парижского конгресса немец Курт Гёдель в серии работ, известных как «Теорема Гёделя о неполноте», формально доказал, что, пользуясь имеющимся у математики логическим инструментарием, непротиворечивость аксиом арифметики доказать невозможно!
Примечательно, что само доказательство теоремы Гёделя относительно несложно. Его идея — в построении в рамках формальной арифметики парадоксального утверждения, напоминающего утверждение из известного парадокса лжеца: «Данное высказывание — ложно», истинность или ложность которого заключить невозможно.
Можно предположить, что столь продолжительное невежество в столь фундаментальном вопросе связано со свойством человеческого сознания, известного в современной когнитивной науке как предвзятость подтверждения. Наш разум имеет тенденцию в первую очередь искать подтверждение тому, в чем мы заранее уверены. Даже если для этого мало оснований и факты, доказывающие несостоятельность нашей позиции, очевидны и находятся на самом виду, мы склонны их не замечать.
Хотя доказательство теоремы Гёделя, несомненно, стало для математики значительным идеологическим кризисом, на научный процесс оно повлияло мало. Невозможность выяснить наверняка, противоречивы ли аксиомы, на которые опирается практически любое математическое исследование, не означает, что эти аксиомы нельзя использовать. Это можно делать до тех пор, пока мы не столкнемся с противоречием, а это вряд ли случится в обозримом будущем. Если же подобный казус все же произойдет, велика вероятность, что путем небольшой корректировки аксиом ход рассуждений удастся оставить без существенных изменений. Кроме того, излишнее внимание к философским вопросам среди серьезных математиков, как правило, считается дурным тоном, что для науки, скорее всего, к лучшему.
И все же этот кризис подтолкнул математическое сообщество к пониманию, что время, когда к математической теореме можно было относится как к истине в последней инстанции, уходит. Математика отчасти лишилась роли безупречного научного языка, возможности смотреть свысока на науки, готовые принимать за истину не то, что доказано, а то, что вытекает из эксперимента и здравого смысла.
Если теорема Гёделя о неполноте повлияла на отношение к строгому доказательству скорее в психологическом смысле, то другой большой кризис сделал изменение отношения к этому понятию неизбежным и стал одной из главных причин постепенного принятия математическим сообществом необходимости использования компьютеров в доказательствах.
Одна из крупнейших математических проблем, интересовавшая ученых на протяжении 1970–1980-х годов, — задача классификации простых конечных групп. Не вдаваясь в подробности, достаточно сказать, что эта задача столь же важна, сколь и трудоемка. Трудоемка настолько, что ее пришлось разбить на множество независимых задач, которые были разделены между группами математиков по всему миру. Эти группы одновременно работали более 10 лет, и сообща классификацию удалось более-менее закончить, хотя для доказательства существования одной из простых конечных групп, получившей прозвище «монстр», пришлось воспользоваться компьютером.
Немного позже был найден путь доказательства существования «монстра», не использующий компьютерные вычисления. Желая «добить» классификацию и доказать ее на основе традиций чистой математики, ученые бросили на это доказательство большие силы, но не только не сумели его завершить, но и нашли серьезные пробелы в доказательствах других, уже принятых частей классификации. Некоторые прорехи удалось сразу заделать, но на исправление отдельных ошибок потребовались колоссальные усилия, на которые ушли еще годы работы. В итоге запись общего доказательства классификации простых конечных групп заняла бы около 20 полных томов, из которых, впрочем, опубликовано только пять, и вряд ли когда-либо будут опубликованы остальные. Теорема считается доказанной, но представление о строгости этого доказательства, столь важной в понятии математиков времен Гильберта, основано только на вере группы работавших над ним ученых, причем ни один из них не способен поручиться за правильность всего доказательства целиком (а некоторые из них в этом даже сомневаются).
Идут годы, и ученые, работавшие над этим глобальным проектом, уходят из математики или из жизни. Их ученики уже не так заинтересованы в технически сложной и вышедшей из моды проблеме. Надежда на то, что человечество когда-либо сможет считать классификацию простых конечных групп наверняка доказанной, очень мала. Тем не менее результат активно используется и в теории групп, и в других разделах математики.
Британский ученый, профессор Королевского колледжа Лондона Брайан Дэвис в своей известной статье «Куда движется математика?» назвал «вторым кризисом математики» кризис переусложненности. За последние 100 лет математика стала слишком большой и разветвленной наукой, содержащей слишком много узкоспециализированных разделов, разобраться в которых способны только небольшие группы работающих в них экспертов. В 1900 году практически каждый из присутствующих на математическом конгрессе ученых на достаточно высоком уровне знал всю математику. Это, в частности, означало, что доказательства, сделанные в том или ином разделе, могли быть проверены достаточно большим числом представителей математического сообщества, а значит, общепризнанны. В наше время это немыслимо, и когда доносится весть, что доказана та или иная теорема, математикам обычно приходится просто полагаться на профессиональное мнение очень узкой группы ученых, которые, кто знает, могли где-то и ошибиться. Как мы видели на примерах классификации простых конечных групп, теоремы о четырех красках и гипотезы Кеплера, растет сложность (и даже буквально — длина) самих доказательств. Для того чтобы проверить правильность четырехсотстраничных выкладок, ставших плодом десятилетнего труда одного человека, может не хватить и пяти лет напряженной работы целой группы математиков, которые к тому же с большим удовольствием занимались бы написанием своих собственных фолиантов.
В современной математике есть множество разделов, которые по-прежнему развиваются по законам классической, чистой науки, не требуют компьютерных вычислений и не содержат неудобоваримых многотомных доказательств. Но в целом математики больше не могут позволить себе отвергнуть использование компьютера только по той причине, что оно не соответствует научным традициям. Роль компьютерных вычислений все равно пока сводится в основном к техническим расчетам, но есть и перспективное направление — создание компьютерных алгоритмов, способных выполнять формальную проверку правильности человеческих доказательств.
Переусложнение науки, неуемный рост технической трудности доказательств, справляться с которой приходится с помощью вычислительных машин, может означать, что математика подошла к пределу потенциала собственных идей, базы своих аксиом и своего традиционного языка. Математика больше не является той наукой, которая поступательно развивалась со времен Евклида до первой четверти XX века. В каком-то смысле она находится в положении физики начала прошлого столетия, когда стало очевидно, что идей Ньютона перестало хватать для описания мира. Может быть, математике суждено совершить прорыв, который даст науке новое понятие о логике и природе математических объектов. И тогда найдутся изящные и короткие доказательства теоремы о четырех красках, теоремы об упаковках шаров и теоремы о числе подсказок в судоку.
