Величайшие математические задачи - Йен Стюарт

В 1999 г. Хейлс подал подготовленное доказательство в Annals of Mathematics, и журнал специально для этого случая набрал жюри из 12 экспертов. К 2003 г. оно объявило, что «с уверенностью на 99 %» представленное доказательство верно. Оставшийся 1 % неуверенности касался компьютерных расчетов; многие из них жюри повторило, а также иными способами проверило стратегию и тактику доказательства, но некоторые его аспекты проверить не удалось. После значительной задержки журнал опубликовал работу. Хейлс признал, что такой подход к доказательству, вероятно, никогда не будет признан на 100 % корректным, и в 2003 г. объявил о старте проекта по переформатированию доказательства в такой вид, в котором его сможет проверить компьютер при помощи стандартных программ автоматической проверки доказательств.

Это может показаться чем-то вроде перехода из огня в полымя, но на самом деле все предельно понятно и логично. Доказательства, которые математики публикуют в журналах, призваны убеждать людей. Как я уже говорил в главе 1, доказательство — это своего рода рассказ. Компьютеры не сильны в литературе, зато прекрасно справляются с заданиями, которые нам не по зубам: они способны безошибочно выполнять длинные нудные расчеты. Компьютеры идеально сочетаются с формальным определением доказательства в университетских учебниках: серия логических шагов, каждый из которых вытекает из предыдущих.

Компьютерщики научились использовать эту способность. Чтобы проверить доказательство, заставьте компьютер проанализировать каждый логический шаг. Звучит просто, но на самом деле доказательства в журналах пишут не так. Эти рассказы оставляют за скобками все рутинное или очевидное… Все привыкли к традиционным фразам: «Несложно убедиться, что…», «Используя методы Чизбургера и Чипса, модифицированные так, чтобы учитывать изолированные сингулярности, видим, что…», «Несложный расчет показывает…». Компьютеры (пока) с подобными задачами не справляются. Но люди-то всегда могут переписать доказательство, заполнив все подобные пропуски, и тогда компьютер вполне может проверить каждый его шаг.

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

В последние годы таким образом были проверены доказательства многих ключевых математических теорем. Для этого их нередко требовалось перевести в другую форму, более подходящую для компьютерных манипуляций. Один из последних триумфов — проверка и подтверждение доказательства теоремы Жордана: всякая замкнутая кривая без самопересечений на плоскости делит плоскость на две связные области. Утверждение может показаться очевидным, но пионеры топологии долго не могли строго доказать его. В конце концов это удалось в 1887 г. Камилю Жордану, опубликовавшему доказательство на 80 страницах, но позже его нередко критиковали за необоснованные ограничения. Поэтому слава досталась Освальду Веблену, давшему в 1905 г. более подробное доказательство. Веблен заявил: «[Жорданово] доказательство… не удовлетворяет многих математиков. В нем теорема принимается без доказательства в существенном особом случае, когда речь идет о простом многоугольнике; что же касается дальнейшего изложения, то следует признать по крайней мере, что не все детали в нем приведены».

Математики без колебаний приняли критику Веблена, но недавно Хейлс еще раз проанализировал доказательство Жордана и не нашел в нем «ничего, на что можно было бы возразить». Более того, замечание Веблена о многоугольнике звучит странно: теорема для него достаточно прозрачна, да и доказательство Жордана вовсе не опирается на этот частный случай^{22}. У доказательств-рассказов есть собственные проблемы. С ними надо держать ухо востро и проверять, совпадает ли популярная версия рассказа с его оригинальным вариантом.

В процессе работы над гипотезой Кеплера Хейлс получил в 2007 г. формальное, проверенное компьютером доказательство теоремы Жордана, на что потребовалось 60 000 строк компьютерного кода. Вскоре после этого группа математиков, воспользовавшись другим программным обеспечением, получила другое формальное доказательство. Компьютерная проверка не застрахована от ошибок на 100 %, но то же можно сказать и о традиционных доказательствах. Более того, многие математические научные труды, вероятно, содержат технические ошибки. Время от времени такие ошибки обнаруживаются и в большинстве случаев оказываются безвредными. Серьезные ошибки, как правило, замечают раньше, чем они приводят к нарушениям и делают что-то явно бессмысленным. Это еще один недостаток доказательства-рассказа — плата за то, что доказательство делается понятным человеку: иногда нестрогая логика выглядит на первый взгляд очень убедительно.

Хейлс называет свой подход Project FlysPecK. Согласно первоначальной оценке, работа над ним должна была занять около 20 лет. За первые девять лет достигнут очень существенный прогресс, так что проект может завершиться досрочно.