Кеннет Аппель

Первое в истории доказательство, существенная часть которого выполнена машиной и не может быть проверена человеком за разумное время. Спор о том, доказательство ли это, идёт до сих пор.

До Иллинойса

Родился в 1932 году в Бруклине, в семье еврейских эмигрантов из Восточной Европы. Работал актуарием и школьным учителем, служил в армии в Форт-Беннинге, затем поступил в аспирантуру Мичиганского университета, где в 1959 году защитил диссертацию по теории групп у Роджера Линдона.

Два года после этого он работал в Institute for Defense Analyses в Принстоне — над криптографией; о содержании работы говорить было нельзя. В 1961 году перешёл в Иллинойсский университет в Урбане и остался там на тридцать два года.

Занимался он теорией групп и вычислимостью: проблема слов, разрешимость, алгоритмические вопросы. К графам пришёл поздно и, по собственным словам, случайно — просто Вольфганг Хакен, сидевший на том же факультете, искал человека, умеющего программировать.

Четыре краски

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

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

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

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

Факультет перенастроил свой почтовый штемпель: FOUR COLORS SUFFICE. Штемпель этот теперь в Смитсоновском музее.

Спор

Приняли доказательство далеко не все. Возражения были двух родов.

Практические: в программе может быть ошибка, в компиляторе может быть ошибка, в железе может быть ошибка. Возражение справедливое — ошибки в правилах разрядки действительно находили, и все они оказались исправимы; в 1989 году Аппель и Хакен выпустили книгу на 741 странице с полным выверенным изложением.

Принципиальные: доказательство должно объяснять, почему утверждение верно, а перебор ничего не объясняет. Это возражение никуда не делось. Роберт Робинсон и соавторы в 1996 году построили новое доказательство — вчетверо короче, но всё равно машинное; в 2005 году Жорж Гонтье проверил его целиком в системе Coq, сняв практические возражения окончательно и не сняв принципиальных вовсе.

Аппель к спору относился спокойно и говорил, что математики просто не привыкли, а привыкнут.

После

В 1993 году он перешёл в Университет Нью-Гэмпшира, где заведовал математическим отделением до 2002 года. Занимался школьным математическим образованием, вёл кружки для одарённых детей, был избран в городской совет Дувра и служил в нём несколько сроков.

Коллекционировал марки, играл в го и в покер и, по свидетельствам, готовил превосходно.

Умер в Дувре в апреле 2013 года от рака пищевода, восьмидесяти лет.