Машина проверяет математику

Что именно оставалось непроверенным

К 1996 году теорема о четырёх красках была доказана дважды — Аппелем и Хакеном, а затем заново Робертсоном, Сандерсом, Сеймуром и Томасом. Оба раза спорили об одном: можно ли верить машине, перебравшей конфигурации.

Спор был поставлен неточно. В обоих доказательствах машина отвечала за меньшую и более надёжную половину работы. Большая половина — рассуждение о том, что такое плоская карта, почему достаточно триангуляций, отчего правила разрядки дают неизбежное множество — была написана людьми на обычном математическом языке. И ошибки находили именно в ней: Хивуд нашёл ошибку у Кемпе через одиннадцать лет, Робертсон с соавторами — несколько ошибок в правилах разрядки Аппеля и Хакена через двадцать.

То есть проверять надо было не программу, а прозу. Прозы было семьсот сорок одна страница.

Как убрать топологию из теоремы про карты

Формальное доказательство нельзя начать словами «рассмотрим карту». Машине нужно определение, а честное топологическое определение плоской карты немедленно тянет за собой теорему Жордана — то самое утверждение, которое очевидно на картинке и мучительно в доказательстве.

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

Остаётся сказать, какие гиперкарты считать плоскими. И вот ответ, ради которого стоило заводить эту нить: плоская — та, для которой выполняется формула Эйлера. Соотношение $V-E+F=2$ работает здесь не как следствие планарности, а как её определение.

Формула, найденная Эйлером в 1750 году — через четырнадцать лет после прогулки по мостам и ровно в том же жанре «считать, не измеряя», — через двести пятьдесят пять лет оказалась тем местом, где машине объясняют, что такое плоскость. Чтобы связать этот глобальный критерий с наглядной геометрией, Гонтье доказал его равносильность локальному — «свойству ЖорданаКамиль Жорданфранцузский математик, инженер путей сообщения · 1838–1922Написал книгу, после которой теорию Галуа стало возможно выучить, и доказал утверждение о том, что замкнутая кривая делит плоскость, — оказавшееся неожиданно трудным. для гиперкарт». Сама теорема Жордана в полном виде так и не понадобилась.

Вычисление как шаг доказательства

Вторая идея убрала границу между «математической» и «машинной» частями.

В Coq доказательство — это программа, а доказываемое утверждение — её тип; это соответствие называется изоморфизмом Карри — Ховарда. Значит, если свойство разрешимо, его проверку можно сделать не внешним счётом, которому верят на слово, а шагом самого доказательства: утверждение «эта конфигурация сводима» превращается в вычисление, а доказательством служит то, что вычисление вернуло «истину». Приём называется вычислительным отражением.

После этого вопрос «доверяете ли вы программе, считавшей конфигурации» исчезает вместе с программой. Считает ядро Coq — ровно то же, что проверяет все остальные шаги.

За основу Гонтье взял не первое доказательство, а второе: робертсоновские 633 конфигурации и 32 правила разрядки вместо 1936 конфигураций Аппеля и Хакена. Алгоритмы поиска конфигураций пришлось переписать заново — трюки с целочисленным кодированием, на которых держится быстрый код на C, внутри системы доказательств не работают. Работа, начатая вместе с Бенжаменом Вернером, заняла несколько лет и закончилась в 2005 году: около шестидесяти тысяч строк, проверенных Coq версии 7.3.1.

Что осталось прочитать глазами

Формальная проверка не отменяет доверия — она собирает его в одну точку. Верить приходится двум вещам.

Первая — ядро: несколько тысяч строк, которые проверяют типы. Оно маленькое нарочно; это называется критерием де Брёйна — проверяющая часть должна быть такой, чтобы один человек мог прочитать её целиком. И её переписывали независимо: чужая программа-проверяльщик принимает те же доказательства.

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

Обмен выгодный. Но заметим честно: доверия не избежать нигде, формализация меняет его количество, а не природу.

Побочный продукт, оказавшийся важнее

Чтобы написать это доказательство, Гонтье пришлось изобрести способ писать доказательства: язык тактик SSReflect и библиотеку Mathematical Components — аккуратную формализацию конечной математики, от списков до теории групп.

Через семь лет тот же коллектив — Гонтье и около пятнадцати человек в совместном центре Microsoft Research и INRIA под Парижем — закрыл этим инструментом теорему ФейтаУолтер Фейтамериканский математик · 1930–2004Вместе с Томпсоном доказал, что всякая конечная группа нечётного порядка разрешима. Статья заняла 255 страниц и целый выпуск журнала — и с неё началась классификация конечных простых групп. — ТомпсонаДжон Григгс Томпсонамериканский математик · род. 1932Доказал вместе с Фейтом, что всякая конечная группа нечётного порядка разрешима, — работа заняла 255 страниц и целый выпуск журнала — и этим открыл дорогу к классификации конечных простых групп.: всякая конечная группа нечётного порядка разрешима. Двести пятьдесят страниц исходного текста плюс два учебника предварительных сведений; в 2012 году всё это стало проверенным формально.

Правило, которое с тех пор подтвердилось не раз: главный результат проекта формализации — не проверенная теорема, а библиотека, оставшаяся после.

Что стало нормой

Гипотеза КеплераИоганн Кеплернемецкий астроном и математик · 1571–1630Вывел законы движения планет из чужих наблюдений, посчитал объём винной бочки способом, из которого через полвека вырастет интеграл, и защищал мать на процессе о колдовстве. об укладке шаров, доказанная Хейлзом в 1998 году с такой же машинной частью и таким же скандалом, полностью формализована к 2014-му. С конца 2010-х центр тяжести переехал в систему Lean с библиотекой mathlib; в 2021–2022 годах там формально проверили ключевую теорему из свежей работы Шольце — по просьбе самого автора, не уверенного в собственном доказательстве.

Тот же изоморфизм Карри — Ховарда, продолженный до конца, дал новые основания математики, где равенство понимается как путь, — и первые библиотеки для них писались опять-таки в Coq. А сам Coq в 2025 году сменил имя на Rocq Prover: инструмент дожил до стадии, когда его переименовывают ради удобной вывески.

Развязка — обе

Нить кёнигсбергских мостов кончается дважды, и оба конца возвращаются к завязке.

Топологическая ветвь замыкается географически: вопрос, поставленный ПуанкареАнри Пуанкарефранцузский математик, физик и философ науки · 1854–1912Последний универсал математики: создал топологию, увидел хаос там, где все видели порядок, и подошёл к теории относительности вплотную, не сделав последнего шага. в Париже, решён в Санкт-Петербурге — в городе, где ЭйлерЛеонард Эйлершвейцарский математик, работавший в Петербурге и Берлине · 1707–1783Самый плодовитый математик в истории: около 900 работ, половина языка современной математики — от знака $\pi$ до записи $f(x)$ — и способность считать, не глядя. разбирал мосты.

Графовая ветвь замыкается по существу: машина, проверяющая теорему о раскраске карт, узнаёт плоскость по формуле Эйлера для многогранников. Две задачи, которые в 1736 и 1750 годах не относились ни к какому разделу математики, в развязке держат друг друга.

И отдельно — про «Calculemus!». ЛейбницГотфрид Вильгельм Лейбницнемецкий философ, математик и дипломат · 1646–1716Придумал знаки $d$ и $\int$, которыми мы пишем анализ до сих пор, — и всю жизнь искал язык, на котором спор можно было бы заканчивать словами «посчитаем». хотел двух вещей: языка, на котором всякое утверждение записывается точно, и машины, которая по этой записи решает, верно оно или нет. Вторую половину закрыли Гёдель и Тьюринг: машины, находящей доказательства, не существует. Первая же сбылась буквально — и почти незаметно.

Проверять машина умеет. Искать по-прежнему приходится человеку: в 1976 году в Урбане неизбежное множество искали люди, а машина считала. Это и есть точный ответ на вопрос, заданный 21 июня 1976 года. Доказательство не перестало быть человеческим делом — просто у него появился корректор, который не устаёт.

Задача. На торе формула Эйлера даёт $V-E+F=0$. Докажите, что любая карта на торе раскрашивается в семь красок.
(Ответ: достаточно триангуляций — добавление рёбер задачу только усложняет. В триангуляции $3F=2E$; подстановка в $V-E+F=0$ даёт $E=3V$, поэтому сумма степеней вершин равна $2E=6V$, а средняя степень — ровно $6$. Значит, вершина степени $\leqslant 6$ есть всегда — и есть она в любом подграфе, потому что подграф тоже лежит на торе. Удаляйте такие вершины по одной, а потом возвращайте в обратном порядке: у каждой возвращаемой вершины занято не более шести цветов, и седьмой свободен. Семь — граница точная: на торе размещаются семь попарно соседних стран, так что меньшим числом красок не обойтись.)

Соседние точки: Урбана (1976) → Coq (2005) — развязка нити кёнигсбергских мостов; вторая её ветвь кончается в Санкт-Петербурге.