Воеводский: гомотопии в алгебре и логике

Первая жизнь: гомотопии в алгебраической геометрии

Владимир Александрович Воеводский (1966–2017) учился в Москве, защитил диссертацию в Гарварде и с 2002 года был профессором Института перспективных исследований в Принстоне.

Замысел первой его программы прост на словах и труден по существу: перенести аппарат теории гомотопий в алгебраическую геометрию.

В топологии всё строится на понятии непрерывной деформации, а для деформации нужен отрезок $[0,1]$. В алгебраической геометрии отрезка нет: там есть только алгебраические многообразия. Воеводский и Фабьен Морель (1998–1999) предложили считать «отрезком» аффинную прямую $\mathbb{A}^{1}$ — и построили на этом полноценную гомотопическую теорию, где работают все привычные конструкции: пространства петель, спектры, обобщённые теории когомологий.

Главный результат — гипотеза МилнораДжон Милнорамериканский математик · 1931–2025Нашёл семимерные сферы, гомеоморфные обычной, но не диффеоморфные ей, — и обнаружил этим, что топологическая структура и гладкая не одно и то же. Пытался доказать противоположное. (1970), связывающая три совершенно разные вещи: K-теорию Милнора поля по модулю 2, когомологии ГалуаЭварист Галуафранцузский математик · 1811–1832За двадцать лет жизни успел провалить экзамены, отсидеть в тюрьме и создать теорию групп — записанную начисто в ночь перед дуэлью. и квадратичные формы. Доказана в 2000 году с помощью построенной техники; Филдсовская медаль 2002 года. Позже (с Роста) была доказана и её обобщённая версия — гипотеза Блоха — Като.

Здесь стоит остановиться на том, что произошло. Инструмент, выросший из мостов Кёнигсберга и ленты Мёбиуса, оказался пригодным для утверждений о полях и квадратичных формах, где никакой непрерывности нет вовсе. Это, пожалуй, самая длинная дуга переноса на всей карте.

Перелом

В середине 2000-х Воеводский пережил то, что сам называл кризисом доверия к собственной работе.

Он обнаружил ошибку в статье 1990 года, написанной вместе с Михаилом Капрановым, — о связи между $\infty$-группоидами и гомотопическими типами. Ошибка стояла незамеченной больше десяти лет, работа цитировалась, на неё опирались. Позже нашлись проблемы и в других местах.

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

Проблема была в том, что существующие системы формальной проверки (основанные на теории множеств или на обычной теории типов) плохо подходили для той математики, которой он занимался: в них не удавалось естественно выразить, что два изоморфных объекта — «одно и то же».

Вторая жизнь: унивалентные основания

Решение оказалось неожиданным и напрямую топологическим.

В теории типов есть тип равенства: для двух объектов $a,b$ типа $A$ существует тип $\mathrm{Id}_A(a,b)$ — «доказательства того, что $a$ равно $b$». Естественно было бы считать, что таких доказательств не больше одного. Но в формальной системе это не выводится — и, как заметили Хофманн и Штрайхер ещё в 1998 году, можно построить модель, где их много.

Воеводский увидел, что это описывает знакомую картину:

Доказательство равенства — это путь. Два доказательства равны, если пути гомотопны. Логика оказалась устроена как топология, причём буквально: ∞-группоид путей — это и есть структура типа.

Отсюда — аксиома унивалентности:

Тождество типов — это то же самое, что эквивалентность между ними.

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

Программа получила название унивалентных оснований математики, а сама теория — гомотопической теории типов (HoTT). В 2012–2013 годах в Институте перспективных исследований прошёл специальный год, собравший математиков, логиков и специалистов по информатике; итогом стала коллективно написанная книга «Homotopy Type Theory» (2013), выложенная свободно.

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

Почему эта точка стоит в топологии

Возражение возможно: при чём тут топология, если речь о логике?

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

Оснований математики предлагалось немного: теория множеств ЦермелоЭрнст Цермелонемецкий математик и логик · 1871–1953Доказательством на одну страницу вызвал самый громкий скандал в основаниях математики за век — и, отбиваясь от критиков, выписал теорию множеств списком аксиом. На этом списке математика стоит по сей день. — Френкеля, теория категорий, теория типов. Гомотопическая теория типов — единственное из них, выросшее из топологии.

Человек

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

Он умер внезапно, в 2017 году, в возрасте пятидесяти одного года. Программа унивалентных оснований продолжается без него; проверяемая машиной математика из экзотики становится обычной практикой — и первым большим примером тут была теорема о четырёх красках, следом — теорема о жордановой кривой и гипотеза КеплераИоганн Кеплернемецкий астроном и математик · 1571–1630Вывел законы движения планет из чужих наблюдений, посчитал объём винной бочки способом, из которого через полвека вырастет интеграл, и защищал мать на процессе о колдовстве., а дальше всё больше рутинных результатов.

Задача. В теории множеств группа $\mathbb{Z}/2$, заданная как $\{0,1\}$ со сложением по модулю 2, и группа $\{+1,-1\}$ с умножением — разные множества, хотя изоморфные. Объясните, что меняет аксиома унивалентности, и почему это удобно.
(Ответ: при унивалентности изоморфизм даёт равенство типов, поэтому всякое утверждение, доказанное для одной группы, автоматически переносится на другую — без отдельной проверки «инвариантности относительно изоморфизма». Именно эти проверки составляют значительную часть рутины в обычных основаниях.)

Следующая точка: Санкт-Петербург — где вопрос, заданный ПуанкареАнри Пуанкарефранцузский математик, физик и философ науки · 1854–1912Последний универсал математики: создал топологию, увидел хаос там, где все видели порядок, и подошёл к теории относительности вплотную, не сделав последнего шага. в 1904 году, наконец получит ответ.