Урбана: четыре краски доказаны машиной

Что оставалось доказать

Вопрос Гатри — хватает ли четырёх красок для любой карты — к 1976 году имел за плечами долгую историю: «доказательство» Кемпе 1879 года, одиннадцать лет считавшееся верным, ошибку, найденную Хивудом в 1890-м, и теорему о пяти красках, спасённую из обломков.

Дальше сто лет накапливалась техника. К середине века было ясно, каким должно быть доказательство. Не хватало только вычислительных сил.

Две идеи

Рассуждение строится от противного. Пусть теорема неверна; возьмём минимальный контрпример — карту, которой не хватает четырёх красок, с наименьшим возможным числом стран. (Достаточно рассматривать триангуляции: любую карту можно доразбить до состояния, когда в каждой вершине сходятся ровно три страны, и от этого задача только усложняется.)

Вводятся два понятия.

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

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

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

У Кемпе неизбежное множество состояло из четырёх конфигураций — вершина степени 2, 3, 4 или 5, — и он умел сводить первые три. Ошибка была ровно в четвёртой.

Разрядка

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

В планарной триангуляции с $V$ вершинами, $E$ рёбрами и $F$ гранями каждая грань окружена тремя рёбрами, а каждое ребро принадлежит двум граням, так что $3F=2E$. Подставим в формулу Эйлера $V-E+F=2$:

$$V-E+\frac{2E}{3}=2\ \Longrightarrow\ E=3V-6 .$$

Сумма степеней вершин равна $2E=6V-12$. Припишем каждой вершине заряд $6-\deg v$. Тогда суммарный заряд равен

$$\sum_v\,(6-\deg v)=6V-(6V-12)=\mathbf{12}.$$

Двенадцать — всегда, в любой триангуляции. Значит, вершины с положительным зарядом — то есть степени 5 и меньше — есть обязательно.

Отсюда и метод разрядки, предложенный Генрихом Хеешем в 1960-е годы. Заряд перераспределяют по фиксированным правилам («вершина степени 5 отдаёт по $\tfrac15$ каждому соседу степени $\geqslant7$» и тому подобное). Сумма при этом не меняется — она по-прежнему 12. Если после перераспределения всякая вершина с положительным зарядом обязана лежать внутри одной из ваших конфигураций, множество неизбежно.

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

1936 конфигураций

Кеннет Аппель и Вольфганг Хакен взялись за это в Иллинойсском университете в 1972 году; в алгоритмической части им помогал аспирант Джон Кох.

Работа шла не так, как обычно представляют. Это не был один прогон программы: неизбежное множество и правила разрядки перестраивались десятки раз, программа сообщала, где список не сходится, авторы правили правила, счёт запускался заново. По собственному признанию Аппеля, машина «подсказывала» им, куда двигаться, — то есть выступала не калькулятором, а собеседником.

К июню 1976 года сошлось: 1936 конфигураций (позже число сократили до 1476), около 1200 часов машинного времени на университетских машинах IBM.

21 июня 1976 года Аппель написал на доске математического факультета: «Modulo careful checking it appears that four colors suffice» — «с точностью до тщательной проверки, похоже, четырёх красок хватает». Почтовое отделение Урбаны завело штемпель FOUR COLORS SUFFICE, и факультет много лет штемпелевал им исходящие письма.

Объявление вышло в Bulletin of the AMS, полное изложение — двумя статьями в Illinois Journal of Mathematics в 1977 году. В обеих потом находили ошибки в правилах разрядки; все они оказались исправимы, и в 1989 году Аппель и Хакен выпустили книгу на 741 странице с полным выверенным рассуждением.

Скандал

Реакция была не восторженной, а растерянной, и растерянность была честной.

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

Возражения были двух видов.

Первое: доказательство должно объяснять. Хорошее доказательство даёт понять, почему утверждение верно. Здесь понимания нет: четырёх красок хватает потому, что 1936 случаев проверены и ни один не подошёл. Это возражение никуда не делось и сегодня.

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

1996: шестьсот тридцать три

В 1996 году Нил Робертсон, Дэниел Сандерс, Пол Сеймур и Робин Томас переделали доказательство целиком. У них 633 конфигурации и 32 правила разрядки вместо сотен, а доказательство неизбежности устроено так, что проверяется независимой программой, которую нетрудно написать заново.

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

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

2005: машина проверяет машину

Последнюю точку поставил Жорж Гонтье: в 2005 году он вместе с Бенжаменом Вернером формально проверил всё рассуждение в системе Coq. Машина проверила машину — и на этот раз проверяющая программа сама была построена так, что доверять надо только её ядру в несколько сотен строк.

С этого момента спор изменил форму. Вопрос «можно ли верить компьютерному доказательству» превратился в вопрос «доверяете ли вы ядру Coq», а это уже обычный технический вопрос с обычным ответом.

Что изменилось

За тридцать лет машинное доказательство перестало быть скандалом и стало нормой.

Гипотеза КеплераИоганн Кеплернемецкий астроном и математик · 1571–1630Вывел законы движения планет из чужих наблюдений, посчитал объём винной бочки способом, из которого через полвека вырастет интеграл, и защищал мать на процессе о колдовстве. об укладке шаров, доказанная Хейлзом в 1998 году с такой же машинной частью и такими же спорами, была полностью формализована к 2014-му. Теорема ФейтаУолтер Фейтамериканский математик · 1930–2004Вместе с Томпсоном доказал, что всякая конечная группа нечётного порядка разрешима. Статья заняла 255 страниц и целый выпуск журнала — и с неё началась классификация конечных простых групп. — ТомпсонаДжон Григгс Томпсонамериканский математик · род. 1932Доказал вместе с Фейтом, что всякая конечная группа нечётного порядка разрешима, — работа заняла 255 страниц и целый выпуск журнала — и этим открыл дорогу к классификации конечных простых групп. о разрешимости групп нечётного порядка формализована в 2012-м. Сегодня существуют библиотеки формализованной математики объёмом в миллионы строк, и в них уже попадают результаты, доказанные только что.

Ответ на вопрос «что такое доказательство», который был задан 21 июня 1976 года, оказался практическим: доказательство — это то, что принимает проверяющая программа. Определение обидное, зато работающее.

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

Следующая точка: Стэнфорд — где придумают, как двоим договориться о секрете, ни разу не встретившись и не таясь.