P не равно NP: Доказательство, которое математики не поймут

Классический пример — доказательство существования иррациональных чисел a и b, таких что a в степени b рационально. Рассмотрим √2 в степени √2. Если это число рационально — мы нашли искомое. Если иррационально — возведём его в степень √2 и получим 2, что рационально. В любом случае искомые a и b существуют. Но что именно является ответом — первый вариант или второй — мы не знаем. Доказательство не даёт нам метода, оно просто показывает, что ответ есть где-то там.

Для классического математика это нормальное доказательство. Для Брауэра — шулерство. Вы не сказали, какие именно a и b работают. Вы не построили их. Вы просто развели руками и сказали: «Ну они же где-то есть». Интуиционист требует: предъявите. Или хотя бы скажите, как их искать [68].

Программа Брауэра была грандиозна. Он предлагал перестроить всю математику на новых — конструктивных — основаниях. В этой новой математике:

— Каждое доказательство существования должно предъявлять объект или метод его построения.

— Бесконечность понимается только как потенциальная, а не актуальная. Не «множество всех натуральных чисел», а «процесс порождения натуральных чисел, который никогда не заканчивается».

— Логика должна быть интуиционистской — без закона исключённого третьего, без доказательств от противного, без аксиомы выбора [69].

По сути, Брауэр предлагал именно то, к чему мы пришли в нашем анализе проблемы P vs NP. Он требовал математики с субъектом. Математики, которая помнит о генезисе. Математики, в которой «существует» означает «построено».

И что же сделало математическое сообщество? Оно раздавило Брауэра.

Главным оппонентом Брауэра был Давид Гильберт — тот самый человек, который мечтал превратить математику в автомат для производства истин. Для Гильберта интуиционизм был не просто конкурирующей программой. Это было личное оскорбление.

Гильберт ответил Брауэру с уничтожающей язвительностью, которая сегодня читается как образец академического хамства. Он заявил, что изъять из математики закон исключённого третьего — это всё равно что «запретить боксёру пользоваться кулаками» или «запретить астроному пользоваться телескопом» [70]. Он назвал интуиционизм «попыткой загнать математику в прокрустово ложе философских предрассудков».

Но Гильберт не ограничился риторикой. Он использовал административный ресурс. В 1928 году, когда Брауэр был членом редакционной коллегии престижнейшего журнала «Mathematische Annalen», Гильберт, пользуясь своим влиянием и состоянием здоровья Брауэра (Брауэр болел), организовал его исключение из редколлегии. Формальным поводом стало то, что Брауэр якобы затягивал публикации. Реальной причиной — то, что Гильберт не мог терпеть конкурента [71].

Это был показательный разгром. Математическое сообщество, наблюдавшее за этой дракой, сделало свои выводы. С Гильбертом — слава, гранты, журналы. С Брауэром — изоляция, безработица, забвение. Выбор был очевиден.

Брауэр проиграл по трём причинам.

Во-первых, он был неудобным человеком. Упрямым, резким, не склонным к компромиссам. Он отказывался говорить на языке оппонентов и требовал, чтобы они выучили его язык. В академической политике так не выживают.

Во-вторых, его программа была разрушительной. Если принять интуиционизм всерьёз, то огромная часть математики XX века — весь анализ на основе теории множеств, вся топология с аксиомой выбора, все доказательства от противного — становится недействительной. Это была бы не реформа, а революция. А революций математики боятся больше, чем противоречий.

В-третьих, и это самое важное для нашей темы, — Брауэр не предложил однозначного критерия различимости «построено» и «угадано». Он настаивал на том, что математика должна быть конструктивной, но не дал строгой процедуры проверки конструктивности. Он апеллировал к интуиции, к «человеческому уму», к «деятельности сознания». А это всё ещё слишком размытые понятия для математики, которая хочет быть точной.

Именно здесь гуманитарный метод, который мы обсуждаем в этой книге, может сделать то, чего не смог Брауэр. Он предлагает не просто лозунг «верните субъекта», а конкретную процедуру: наблюдаемость элементарного действия, однозначность метода, превращение желания в потребность через осознание «что я сделал». Это критерии, которые можно применять к конкретным задачам, а не философские пожелания.

Брауэр умер в 1966 году, всеми забытый, в своём доме в голландском Бларикуме. Но его идеи не умерли. Они ушли в подполье, в «параллельную математику», где тихо развивались десятилетиями.

Его ученик Аренд Гейтинг формализовал интуиционистскую логику, показав, что она может быть столь же строгой, как и классическая [72]. Пер Мартин-Лёф создал теорию типов — конструктивную альтернативу теории множеств, где каждое доказательство является программой [73]. Эррет Бишоп в 1967 году опубликовал «Основания конструктивного анализа», где показал, что огромную часть математического анализа можно перестроить на конструктивных основаниях, без аксиомы выбора и закона исключённого третьего [74]. А соответствие Карри-Говарда — формальный мост между доказательствами и программами — стало одним из столпов современной computer science.

Так что Брауэр проиграл битву, но не войну. Его предупреждение было отвергнуто — но не опровергнуто. И сейчас, когда математика упёрлась в проблему P vs NP как в стену, возможно, пришло время перечитать Брауэра заново. Не как исторический курьёз. А как дорожную карту к выходу из тупика.

3.2. Конструктивная математика Маркова и школа Санкт-Петербурга

История конструктивной математики в СССР — это история о том, как идеологическое давление, помноженное на научную честность, иногда даёт парадоксальные результаты. Марксистско-ленинская философия требовала от науки «практической направленности» и «борьбы с идеализмом». Платонизм с его миром идей, где живут математические объекты, был объявлен буржуазным мракобесием. А аксиома выбора — и вовсе поповщиной. Казалось бы, идеальный повод для разгрома всей математики.

Но математики ленинградской школы во главе с Андреем Андреевичем Марковым — сыном того самого Маркова, который придумал цепи, — сделали нечто совершенно неожиданное. Вместо того чтобы проклинать начальство и прятать рукописи под половицу, они построили цельную, логически безупречную альтернативу классической математике, которая не только удовлетворяла требованиям марксистской философии, но и объективно была шагом вперёд по сравнению с интуиционизмом Брауэра.

Брауэр, при всём его героизме, страдал одним недостатком: он был мистиком. Его «интуиция», его «деятельность ума», его «сознание математика» — всё это были понятия, которые невозможно формализовать. Брауэр говорил: «Доказательство — это ментальная конструкция». Но что такое «ментальная конструкция»? Как отличить её от «нементальной»? Где критерий?

Марков и его ученики сделали то, что должны были сделать ещё во времена Брауэра: они выбросили мистику и заменили её строгим, формальным определением конструктивности [75]. Их подход можно сформулировать одной фразой, которая звучит как приговор платонизму: объект существует тогда и только тогда, когда предъявлен алгоритм, который его строит.

Никакого «сознания». Никакой «интуиции». Никакого «мира идей». Только алгоритм. Если вы не можете написать программу, которая за конечное число шагов построит объект, — вы не доказали его существование. Вы просто сотрясли воздух.

Этот подход блестяще решал проблему, которая погубила Брауэра. Брауэр говорил: «Математика — это деятельность ума». Ему отвечали: «А что такое ум?» Брауэр начинал объяснять про интуицию и сознание — и его переставали слушать. Марков сказал: «Математика — это деятельность алгоритма». Ему не могли возразить — потому что алгоритм можно предъявить, запустить, проверить [76].

Конструктивная математика Маркова держалась на трёх принципах, каждый из которых был гвоздём в крышку гроба бессубъектной математики.

Первый принцип: потенциальная осуществимость. Абстракция актуальной бесконечности отвергается. Вместо неё принимается абстракция потенциальной осуществимости: мы можем построить сколь угодно большое натуральное число, но мы никогда не построим «множество всех натуральных чисел» как завершённый объект [77].

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

Второй принцип: отказ от закона исключённого третьего для бесконечных множеств. Здесь Марков наследует Брауэру: утверждение «для всех x выполняется P(x)» не может считаться доказанным, если не предъявлен метод, позволяющий для любого конкретного x проверить, что P(x) истинно. Просто сказать: «Ну не может же быть, чтобы для какого-то x оно было ложно» — недостаточно.

Это отсекает почти все классические доказательства существования, построенные на принципе «если бы объекта не было, мы бы пришли к противоречию». В конструктивной математике Маркова такое рассуждение не проходит. Вы должны предъявить объект. Или хотя бы сказать, как его искать [76].

Третий принцип: алгоритм как критерий существования. Это самое главное. В классической математике существует объект или нет — решают аксиомы. В конструктивной математике Маркова — решает алгоритм. Если вы можете написать программу, которая за конечное число шагов построит объект, — объект существует. Если не можете — извините.

Такой подход радикально меняет статус математика. Из жреца, который созерцает платонические истины, он превращается в инженера, который строит работающие конструкции. Из мистика — в программиста.

Помимо трёх китов, Марков сформулировал ещё один принцип, который стоит особняком и который позже назовут его именем — принцип Маркова [78]. Звучит он так: если алгоритм не может не остановиться, то он остановится.

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

Это был тонкий компромисс между строгим интуиционизмом Брауэра и практическими нуждами реальной математики. Принцип Маркова позволял сохранить часть классических результатов, которые интуиционизм Брауэра безжалостно выбрасывал, и при этом не скатываться обратно в платоническое болото аксиомы выбора.

Западные логики потом долго спорили, является ли принцип Маркова «законным» с точки зрения конструктивизма. Но для самого Маркова и его школы это был не предмет спора, а рабочий инструмент. Они не философствовали о природе истины — они строили работающую математику.

Ленинградская школа конструктивной математики имеет прямое — и убийственное — отношение к проблеме P vs NP. Причём сами марковцы, скорее всего, не думали об этом в таких терминах. Но мы, вооружённые их подходом, можем сформулировать проблему заново.

В классической математике проблема P vs NP звучит так: «Равны ли два класса задач, определённых через квантор существования?» И как мы уже выяснили, ответ на этот вопрос не может быть получен стандартными методами, потому что эти методы не различают типы существования.

В конструктивной математике Маркова эта проблема переформулируется так: «Для любой задачи, решение которой можно быстро проверить, существует ли алгоритм, который быстро это решение строит?»

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

Более того, марковский критерий потенциальной осуществимости даёт нам инструмент для анализа конкретных задач. Для эйлерова цикла мы можем предъявить алгоритм, который за полиномиальное время строит цикл. Для гамильтонова цикла — не можем. Мы можем только перебирать варианты или угадывать. В классической математике и то и другое — «алгоритмы», просто один быстрый, а другой медленный. В конструктивной математике Маркова между ними — пропасть: один строит, другой угадывает.

Так школа Маркова, сама того не подозревая, создала язык, на котором P ≠ NP — это не гипотеза, а почти что тавтология. Потому что «построить за полиномиальное время» и «проверить за полиномиальное время» — это два разных типа существования, и их несовпадение встроено в саму философию конструктивной математики.

Если Марков и его школа были так хороши, почему же их подход не стал мейнстримом? Ответ до обидного прост. Во-первых, они были в СССР, а СССР проиграл холодную войну — в том числе и в математике. После крушения Союза советская математическая школа была частично ассимилирована западной, частично разорена, и её философские основания были объявлены «идеологическим пережитком» [79].

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

В-третьих, конструктивная математика требует от математика больше работы. Неконструктивное доказательство часто короче и проще. Чтобы предъявить алгоритм, нужно попотеть. Чтобы доказать, что алгоритм работает за полиномиальное время, — попотеть вдвойне. Математики, как и все люди, предпочитают лёгкие пути.

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

В самом деле. Что утверждает принцип Маркова? «Если алгоритм не может не остановиться, то он остановится». Звучит как тавтология, как безобидное логическое следствие. Но давайте прочитаем это по частям. «Не может не остановиться» означает: предположение о бесконечной работе приводит к противоречию. Это классическое доказательство от противного — ровно то, с чем боролся Брауэр. Вы не знаете, когда алгоритм остановится. Вы не можете предъявить момент остановки. Вы не можете сказать: «Подожди ещё сто шагов, и он точно встанет». Вы знаете только, что он не может не встать когда-нибудь.

И вы называете это конструктивным знанием?

Принцип Маркова — это та же аксиома выбора, только переодетая в рабочий комбинезон алгоритмиста. Там говорилось: «Функция выбора существует, хоть мы и не знаем, как она работает». Здесь говорится: «Момент остановки существует, хоть мы и не знаем, когда он наступит». Разницы нет. И там, и там вам продают актуальное существование без предъявления, платонический жест в конструктивной упаковке [78]. Это не другое утверждение, это то же самое утверждение, просто адресованное другой аудитории: не теоретико-множественникам, привыкшим к аксиоме выбора, а алгоритмистам, которым аксиома выбора колет глаза, а принцип Маркова — уже нет.

Сам Марков это, разумеется, понимал. Он был слишком хорошим логиком, чтобы не видеть, что он делает. Он не изобрёл новый тип существования. Он просто придумал, как протащить старый платонический трюк через таможню конструктивной математики, завернув его в слово «алгоритм». Без этого трюка слишком многое из привычной математики оказывалось недоказуемым — и он предпочёл сохранить теоремы ценой сохранения платонизма.

Но мы-то с вами уже знаем: маскировка актуальной бесконечности под конструктивность до добра не доводит. Сегодня ты принял принцип Маркова, завтра — аксиому выбора, а послезавтра удивляешься, почему проблема P vs NP не решается. А она не решается именно потому, что математика продолжает протаскивать актуальное существование в конструктивные рассуждения, меняя ему названия, но не меняя сути.

Ленинградская школа, при всех её заслугах, остановилась в шаге от истины. Она нащупала критерий — алгоритм как свидетельство существования, — но не решилась применить его до конца. Она предпочла сохранить часть классической математики ценой сохранения классической слепоты — просто завернув эту слепоту в новую обёртку. А мы теперь расхлёбываем.

Так что школа Маркова осталась маргиналией — уважаемой, но маргиналией. Её результаты вошли в теорию алгоритмов и computer science, но её философия была забыта. А зря. Потому что именно в этой философии — ключ к проблеме P vs NP. Ключ, который математический мейнстрим выбросил, не потрудившись даже понять, от какой двери он был.

3.3. Теория типов Мартин-Лёфа и соответствие Карри-Говарда

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

В классической математике всё является множеством. Число — это множество. Функция — это множество. Отношение — это множество. Даже доказательство — и то, в конечном счёте, всего лишь цепочка символов, которую можно закодировать как множество. Эта онтологическая монотонность очень удобна: если всё — множество, то для всего работают одни и те же аксиомы. Но у этой монотонности есть цена, которую мы уже обсуждали: множество — это родо-видовое понятие. Объект принадлежит множеству или не принадлежит — третьего не дано. А как он туда попал, кто его построил и зачем — это не важно [80].

Мартин-Лёф предложил альтернативу: вместо множеств использовать типы. Тип — это не просто коллекция элементов. Тип — это инструкция по построению этих элементов. Когда вы говорите: «Пусть n — натуральное число», вы в классической математике просто объявляете, что n принадлежит множеству N. В теории типов вы обязаны предъявить, как именно n построено: 0 — это натуральное число (правило введения); если m — натуральное число, то successor(m) — тоже натуральное число (ещё одно правило введения). И никаких других натуральных чисел не существует [81].

Это радикальная смена перспективы. Множество — это мешок, в котором уже лежат все его элементы. Тип — это правило, по которому элементы можно порождать. Множество — актуально. Тип — потенциален. Множество говорит: «Вот что есть». Тип говорит: «Вот как сделать». Мартин-Лёф, сам того, возможно, не подозревая, вернул в математику аристотелевское различие между актуальной и потенциальной бесконечностью — и сделал это на строгом формальном языке [82].

Но настоящая бомба, спрятанная в теории типов, — это не замена множеств типами. Это соответствие Карри-Говарда — открытие, которое показывает, что доказательство теорем и написание программ — это одно и то же.

История этого открытия сама по себе достойна пера драматурга. В 1930-е годы американский логик Хаскелл Карри заметил странную параллель между логическими аксиомами и типами комбинаторов в лямбда-исчислении. В 1960-е годы Уильям Говард, тоже американец, развил эту идею до полноценного изоморфизма: каждой логической связке соответствует типовая конструкция, а каждому правилу вывода — способ построения программы [83]. Но только Мартин-Лёф превратил это наблюдение из курьёза в фундамент целой математической системы.

Суть соответствия проста и убийственна одновременно. Логическая импликация «если A, то B» соответствует типу функции из A в B. Доказать импликацию — значит написать функцию, которая преобразует доказательство посылки в доказательство заключения. Конъюнкция «A и B» соответствует типу пары. Дизъюнкция «A или B» соответствует размеченному объединению. Квантор существования — зависимой паре [84].

Это означает буквально следующее: любое доказательство является программой, а любая спецификация теоремы — типом этой программы. Если вы можете написать программу, тип которой соответствует утверждению теоремы, — вы доказали теорему. Если не можете — не доказали. Точка.

Математики, привыкшие к тому, что доказательство — это текст на естественном языке с вкраплениями формул, восприняли это как акт агрессии. Как это — «доказательство должно компилироваться»? Как это — «проверка доказательства — это проверка типов»? Вы что, предлагаете нам стать программистами? Мы, жрецы платонических истин, должны будем писать код?!

Именно это им и предложили. И они, разумеется, отказались.

Главное преимущество теории типов Мартин-Лёфа перед интуиционизмом Брауэра и даже перед конструктивной математикой Маркова — в том, что конструктивность здесь не является философским пожеланием, пристёгнутым к математике снаружи. Она встроена в сам синтаксис системы.

В классической математике вы можете сказать: «Докажем, что существует объект с таким-то свойством». И доказать это от противного, не предъявляя объекта. В теории типов вы не можете так сказать — потому что тип «существует x, такой что P(x)» определён как тип зависимой пары: вы должны предъявить конкретный элемент a и доказательство того, что P(a) истинно. Если вы не можете предъявить a, вы не можете построить элемент этого типа. Ваше «доказательство» просто не пройдёт проверку типов [81].

Это гениальный ход. Мартин-Лёф не уговаривает математиков быть конструктивными. Он делает неконструктивное рассуждение синтаксически невозможным. Вы не можете написать неконструктивное доказательство в теории типов по той же причине, по которой вы не можете написать программу, которая использует необъявленную переменную: компилятор не пропустит.

Так субъект возвращается в математику — но не как философская метафора, а как программист, пишущий код. Не как «сознание», «интуиция» или «деятельность ума» — а как вполне конкретный человек, сидящий за клавиатурой и набирающий строчки, которые должны скомпилироваться. Теория типов — это математика, в которой без субъекта просто ничего не работает [85].

Если теория типов так хороша, почему же математики до сих пор сидят на ZFC? Ответ одновременно прост и печален.

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

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

В-третьих, — и это самое проблемное, — теория типов не решает проблему P vs NP автоматически. Да, она различает конструктивное и неконструктивное существование. Да, она требует предъявления программы. Но она не говорит, какой длины будет эта программа. Вы можете «предъявить» программу, которая перебирает экспоненциальное число вариантов, — и с точки зрения теории типов это будет корректное доказательство существования. Медленное, но корректное. Теория типов гарантирует конструктивность, но не гарантирует эффективность [86].

И в этом — её ограничение. Как и ленинградская школа, она останавливается в шаге от решения проблемы P vs NP. Она даёт язык, на котором можно говорить о построении. Но она не даёт критерия, отделяющего быстрое построение от медленного. А для этого нужно уже не просто различать «построено» и «угадано». Нужно ещё различать «построено быстро» и «построено медленно». Нужно ввести в математику понятие времени. Понятие усилия. Понятие ресурса.

И здесь мы возвращаемся к гуманитарному методу — потому что именно он, со своим различением предмета и метода, однозначности и неоднозначности, наблюдаемости и фантазирования, может дать недостающий критерий. Но об этом — позже. А пока зафиксируем: Мартин-Лёф и Карри-Говард сделали великое дело. Они показали, что математика может быть конструктивной, не теряя строгости. Они построили мост между логикой и программированием. Им оставалось только понять, что не всякая программа одинаково полезна — и что быстрая программа отличается от медленной примерно так же, как живой тигр от чучела.