Карта → линии → сквозной сюжет

Мечта Лейбница

от «подсчитаем!» до машины, которая проверяет доказательства

1 февраля 1673 года Лейбниц показывает Лондонскому королевскому обществу машину со ступенчатым валиком: она умножает за один приём. Через шесть лет он же набрасывает совсем другое — универсальный язык, на котором всякое рассуждение записывается формулами, и тогда спорящим достаточно сказать друг другу: «Подсчитаем!» Эти две половины одной мысли он не соединил (даже свою двоичную арифметику с валиком так и не связал), а наброски пролежали в архиве двести лет, пока всё не изобрели заново.

Язык. Первым делом логика становится алгеброй: у Буля высказывания складываются и умножаются, и $x^{2}=x$ (1847). Фреге за одну книжку в 88 страниц строит то, чего не было двадцать два века, — язык с переменными, кванторами и правилами вывода (Йена, 1879), а Пеано записывает пятью аксиомами всю арифметику (Турин, 1889). И в 1902-м три строчки в письме Рассела показывают, что из аксиом Фреге выводится противоречие. Язык отстраивают заново — «Principia Mathematica», три тома, «1+1=2» в середине второго.

Ответ. Гильберт требует доказать, что этот язык непротиворечив и что всякий вопрос в нём разрешим механически. 7 сентября 1930 года в Кёнигсберге двадцатичетырёхлетний Гёдель в проходной реплике объявляет, что первое невозможно; Генцен вскоре измерит, насколько именно не хватает средств — программа провалилась не целиком, но провалилась. Остаётся второе, Entscheidungsproblem. Чтобы ответить на него «нет», сначала пришлось сказать, что такое механическая процедура: в 1936 году это сделали трижды и независимо, и все три определения совпали. У Чёрча это язык подстановок, у Тьюринга — описание машины, которой ещё не существует.

Машина. Девять лет спустя чертёж логика становится чертежом инженера: в незаконченном черновике на сто одну страницу фон Нейман описывает машину, у которой команды лежат в той же памяти и в том же виде, что и числа (Филадельфия, 30 июня 1945). Ещё через шесть лет такая машина работает и на континенте — МЭСМ в бывшем монастырском корпусе под Киевом (1948–1951). Дальше вычисление возвращается в математику дважды. Сначала приговором: в обычной алгебре (Новиков, 1955) и в обычной теории чисел (Матиясевич, 1970) есть вопросы, для которых алгоритма нет, — а сам вопрос «можно ли вычислить» сменяется вопросом «сколько это стоит» (Карп, 1972). Потом доказательством: 1936 конфигураций и 1200 часов машинного времени закрывают теорему о четырёх красках (1976), и вместе с ней приходит вопрос, которого математика не знала, — что считать доказательством, если прочитать его не может ни один человек. Через тридцать лет отвечает другая машина: доказательство проверено формально, и доверять надо только ядру проверяющей программы (Coq, 2005). Основания под это Воеводский перестраивает заново — так, чтобы машине было удобно.

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

Открыть на карте

1

Лондон 1 февраля 1673
Лейбниц: ступенчатый валик
Завязка, половина первая: машина, которая умножает сама

Деталь, позволившая умножать за один приём, прожила два с половиной века — до механических калькуляторов 1970-х. Сама машина при этом толком не работала, а свою двоичную арифметику Лейбниц с ней так и не соединил.
2

Ганновер ок. 1679
«Calculemus!»: мечта Лейбница
Завязка, половина вторая: язык, в котором спор решается вычислением. Соединить их автор не стал

Универсальный язык, в котором спор разрешается вычислением: «Подсчитаем!» Наброски остались в архиве и пролежали двести лет, пока всё не изобрели заново. Мечта сбудется наполовину — и доказательство несбыточности второй половины окажется ценнее самой мечты.
3

Корк Линкольн, 1847; Корк, 1854
Буль: законы мысли
Первый шаг к языку: рассуждение становится алгеброй

Сын сапожника, не учившийся в университете ни дня, превращает логику в алгебру, где $x^{2}=x$. Девяносто лет спустя Шеннон покажет: это в точности алгебра релейных схем.
4

Йена 1879
«Begriffsschrift»: вся современная логика в 88 страницах
Язык найден: кванторы и правила вывода, на которых записывается любое доказательство

Малоизвестный доцент из Йены за одну книжку строит то, чего не было двадцать два века: язык с переменными, кванторами и правилами вывода, на котором записывается любое математическое рассуждение. Книжку почти не заметили — отчасти потому, что читать её было физически невозможно.
5

Турин 1889
Пеано: пять аксиом, из которых следует вся арифметика
И на нём записана арифметика — та самая система, о которой через сорок два года скажут, что она неполна

Латинская книжка в три десятка страниц задаёт натуральный ряд списком аксиом, последняя из которых — школьный принцип математической индукции. Заодно там впервые появляются значки $\in$, $\supset$, $\cup$, $\cap$. Именно про эту систему через сорок два года будет доказано, что она неполна.
6

Йена 16 июня 1902
Письмо Рассела: фундамент выбит
Три строчки — и языка нет: из аксиом Фреге выводится противоречие

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

Кембридж т. I — 1910, т. II — 1912, т. III — 1913
«Principia Mathematica»: три тома ради «1+1=2»
Язык отстроен заново — ценой трёх томов ради «1+1=2»

Рассел и Уайтхед десять лет выводят арифметику из чистой логики. Теория типов запрещает парадокс — ценой такой громоздкости, что «1+1=2» доказывается в середине второго тома с пометкой «предложение иногда бывает полезно».
8

Кёнигсберг 7 сентября 1930
Кёнигсберг, 7 сентября 1930
Ответ Лейбницу: нет. Во всякой достаточно богатой системе есть истинные недоказуемые утверждения

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

Гёттинген натуральный вывод и секвенции — 1934–1935, непротиворечивость арифметики — 1936
Генцен: непротиворечивость арифметики, доказанная извне
Но провалилась программа не целиком: измерено ровно, насколько нужно выйти за пределы арифметики

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

Принстон «An unsolvable problem…» — апрель 1936, «A note on the Entscheidungsproblem» — 1936
Чёрч: вычисление как подстановка
Чтобы сказать «алгоритма нет», надо определить алгоритм. Первое определение — язык подстановок, из которого вырастут системы проверки доказательств

За семь месяцев до Тьюринга Алонзо Чёрч отвечает Гильберту «нет» — и делает это на языке, где нет ни чисел, ни машин, а есть только функции и подстановка. Из этого языка вырастут функциональное программирование и системы проверки доказательств.
11

Кембридж 1936
Тьюринг: что такое «вычислить»
Второе определение совпало с первым — и оказалось чертежом машины, которой ещё не было

Чтобы ответить «алгоритма не существует», надо сперва сказать, что такое алгоритм. В 1936 году это сделали трижды и независимо, и все три определения совпали. У Тьюринга определение оказалось не только точным, но и чертежом машины, которой ещё не было.
12

Филадельфия «First Draft of a Report on the EDVAC» — 30 июня 1945
«Первый набросок»: программа переезжает в память
Чертёж логика становится чертежом инженера: программа переезжает в ту же память, где числа

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

Киев 1948–1951
МЭСМ: первая ЭВМ континентальной Европы
И машина собирается взаправду — двенадцатью сотрудниками в бывшем монастыре под Киевом

Двенадцать научных сотрудников в бывшем монастырском корпусе под Киевом за три года собрали машину на шести тысячах ламп. У ENIAC людей было раз в десять больше. Всё это происходило, пока в философских журналах кибернетику называли реакционной лженаукой.
14

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

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

Санкт-Петербург 1970
Десятая проблема Гильберта: ответ — «нет»
И в обычной теории чисел тоже

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

Беркли 1972
NP-полнота: 21 задача — одна проблема
Вопрос меняется: не «можно ли вычислить», а «сколько это стоит»

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

Урбана (Иллинойс) 21 июня 1976
Урбана: четыре краски доказаны машиной
Второе возвращение — уже доказательством: теорема доказана перебором, который человеку не прочитать

1936 конфигураций, около 1200 часов машинного времени — и гипотеза, простоявшая 124 года, доказана. Вместе с ней пришёл вопрос, которого математика прежде не знала: что считать доказательством, если ни один человек не может его прочитать?
18

Кембридж доказательство закончено в декабре 2004, объявлено в апреле 2005
Машина проверяет математику
Мечта сбылась наполовину: спор о том, верно ли доказательство, решается вычислением

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

Принстон мотивные когомологии — 1996–2000; унивалентные основания — 2006–2013
Воеводский: гомотопии в алгебре и логике
И основания переписываются заново — так, чтобы машине было удобно их проверять

Сначала методы теории гомотопий переносятся в алгебраическую геометрию и решают гипотезу Милнора. Потом обнаруживается, что топологически устроена сама логика: типы ведут себя как пространства, а равенства — как пути. Топология, начинавшаяся как раздел геометрии, оказывается кандидатом в основания всей математики.