У Вэньцзюнь: машина доказывает теоремы о треугольнике

Человек

У Вэньцзюнь (1919–2017) — китайский математик, известный сначала совсем другим: в конце 1940-х он учился в Страсбурге и Париже, работал с Эли Картаном и Шиин-Шэнь Черном и получил результаты о характеристических классах, которые называют теперь классами У. Черн на карте есть, и это одна из тех же лабораторий.

В 1951 году он вернулся в Китай. Дальше — Академия наук, а с конца 1960-х долгий перерыв: культурная революция, работа на заводе.

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

К этой мысли он вернётся, когда в Китае появятся вычислительные машины.

Машина и геометрия: что было до

Мысль поручить машине доказательство теорем не нова.

В 1959 году Гербер Гельернтер в IBM построил «Geometry Theorem Prover» — программу, доказывавшую школьные геометрические теоремы перебором с эвристиками: она искала цепочку рассуждений, отсекая заведомо бесплодные ветви с помощью чертежа. Программа работала и производила впечатление, но упиралась в потолок: перебор рос, и на задачах чуть сложнее школьных машина захлёбывалась.

Причина понятна. Программа искала человеческое доказательство — последовательность геометрических шагов. Пространство таких последовательностей огромно, и никакие эвристики его не укротили.

Метод У

В 1977 году У Вэньцзюнь предложил другой ход.

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

Вопрос «следует ли заключение из условий» превращается в вопрос: делится ли многочлен-заключение на систему многочленов-условий? А это уже не поиск, а вычисление — деление с остатком, доведённое до конца по чёткому правилу.

Технически метод опирается на приведение системы к особому виду (характеристическому множеству) — идею, которую в 1930-е годы разрабатывал американский алгебраист Джозеф Ритт и которую после его смерти забыли. У Вэньцзюнь достал её из забвения и довёл до работающего алгоритма.

Результат: машина доказывает сотни классических теорем подряд. Теорему Симсона, теорему Фейербаха, теорему Морли, теорему Паппа — всё, что в этой линии добывалось веками, — за секунды и без единой догадки.

Что это значит

Тут легко впасть в две крайности, и обе неверны.

Первая: «машина заменила геометров». Не заменила. Метод У доказывает заданное утверждение; придумать, что именно стоит доказывать, он не может. Морли нашёл свою теорему, потому что смотрел на трисектрисы, на которые не смотрел никто, — машина не смотрит никуда.

Вторая: «машинное доказательство не настоящее». Настоящее. Оно проверяемо, воспроизводимо и не содержит пробелов — в отличие, скажем, от пяти доказательств Штейнера про изопериметр, в каждом из которых пробел был.

Верное же вот что. Двадцать три века геометры искали в треугольнике красивые рассуждения — короткие, неожиданные, дающие понимание. Метод У показал, что понимание и доказательство — разные вещи: можно получить второе, не получив первого.

Ровно этот вопрос задавал Штейнер, когда отказывался от вычислений. Он считал, что доказательство должно объяснять, а не только удостоверять. Через полтора века выяснилось, что удостоверять можно полностью автоматически — а объяснять по-прежнему некому, кроме человека.

Конец линии

На этом сюжет, начатый таблицей хорд на Родосе, замыкается.

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

Двадцать три века — от инструмента до алгоритма, и в промежутке между ними вся та математика, которую проходят в школе.

Дальше треугольник живёт в учебниках, в олимпиадных сборниках и в энциклопедии центров, где их набралось больше семидесяти тысяч. Истории у него больше нет — и эта линия на нём кончается.