Джордан Элленберг - Как не ошибаться. Сила математического мышления

1,00000000000000000000000000000165 раз,

то есть довольно близко к решетке Лича {197} [239].

Я пойму вас и даже прощу, если вы скажете, что вам, мол, нет никакого дела до двадцатичетырехмерных сфер и того, как можно их упаковать. Но важно понимать один момент: любой математический объект, столь невероятный, как решетка Лича, приобретает весьма большое значение, и к нему д о лжно отнестись крайне серьезно. Как выяснилось, решетка Лича содержит множество симметрий поистине экзотического вида – Джон Конвей, крупный специалист в области теории групп, узнал о ней в 1968 году, за двадцать четыре часа непрерывных вычислений он выписал на огромный рулон бумаги все симметрии решетки Лича {198}. В конечном счете эти симметрии позволили сформулировать последние фрагменты теории конечных групп симметрии, занимавшей умы алгебраистов на протяжении большей части ХХ столетия [240].

Что касается старых добрых трехмерных апельсинов… Оказывается, Кеплер был прав, настаивая, что его способ упаковки самый лучший, но это не было доказано еще целых четыре столетия, пока в 1998 году теорию Кеплера не подтвердил Томас Хейлс, в то время профессор Мичиганского университета. Хейлс решил этот вопрос с помощью сложного и изящного доказательства, в котором задача была сведена к анализу всего лишь нескольких тысяч сфер, выполненному посредством большого объема компьютерных вычислений. Для математического сообщества не проблема создать сложное и изящное доказательство (мы привыкли к такого рода трудам), и эта часть работы Хейлса быстро получила превосходную оценку и подтверждение правильности; но что касается большого объема компьютерных вычислений – тут сложилась более серьезная ситуация. Доказательство возможно проанализировать до последней детали, однако с компьютерной программой все обстоит иначе. Теоретически человек в состоянии проверить каждую строку кода, но, даже если он с этим справится, может ли он полагаться на то, что код будет выполняться корректно?

Почти все математики признали доказательство ученого, но, по всей видимости, самолюбие Хейлса было сильно задето сомнением коллег по поводу того, что при доказательстве ему пришлось воспользоваться компьютерными вычислениями. После подтверждения гипотезы Кеплера он отошел от геометрии, которая сделала его знаменитым, и занялся проектом формальной верификации доказательств. Хейлс предвидит появление математики будущего, отличной от современной, и работает над ее созданием. Он считает, что математические доказательства, независимо от того, как они выполнены – с помощью ли компьютера или с помощью карандаша и бумаги, – стали настолько сложными и взаимозависимыми, что мы больше не можем быть полностью уверенными в их корректности. Классификация конечных простых групп – к настоящему времени завершившийся проект, важной частью которого стал выполненный Конвеем анализ решетки Лича, – состоит из сотен работ сотен авторов. В итоге их труд занимает около десяти тысяч страниц, и не приходится утверждать, что хотя бы один человек из ныне живущих понимает его целиком. Так как мы можем быть уверены в его правильности?

По мнению Хейлса, у нас нет иного выбора, кроме как начать все с самого начала, перестроив всю совокупность математических знаний в пределах формальной структуры, которую можно будет проверять с помощью компьютера. Коль скоро код, проверяющий формальные доказательства, сам поддается проверке (с точки зрения Хейлса, эта цель вполне достижима), мы можем навсегда избавиться от споров вокруг проблемы, с которой столкнулся в свое время Хейлс, – действительно ли доказательство является доказательством. Что будет дальше? Возможно, на следующем этапе появятся компьютеры, способные конструировать доказательства или даже генерировать идеи без какого бы то ни было вмешательства человека.

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