Доказательство в коде: как машина истины трансформирует математику и ИИ- Кевин Хартнетт
В 2013 году исследователь и программист Леонардо (Лео) де Моура начал создавать в Microsoft Research компьютерную программу под названием Lean. Первоначально де Моура искал инструмент для проверки программного обеспечения — так называемую «машину истины», способную на 100% гарантировать, что в коде таких программ, как Microsoft Word или Windows, нет багов и уязвимостей.
Однако инженеры-программисты не спешили массово внедрять Lean. Неожиданно для самого автора потенциал программы распознало совершенно иное сообщество — профессиональные математики, принявшие её с почти мессианским энтузиазмом. Переход от проверки софта к математике оказался абсолютно естественным. В отличие от школьной математики, сосредоточенной на вычислениях, научная математика целиком строится на доказательствах.
Доказательства и компьютерные программы имеют одинаковую природу: и те и другие пишутся с использованием точного синтаксиса в виде последовательности логических шагов. Если логика программы построена верно, она работает без сбоев; если логика доказательства безупречна, на выходе получается новая подтверждённая теорема.
Книга рассказывает о том, как небольшая группа математиков и информатиков — Джереми Авигад, Том Хейлз, Кевин Баззард, Патрик Массо, Йохан Коммелин, Марио Карнейро и другие — вознамерилась произвести крупнейший сдвиг в способе написания и проверки доказательств за всю многотысячелетнюю историю математики. Их целью было создание цифровой математической библиотеки будущего (Mathlib), заполняемой путём кропотливого перевода учебников и научных статей на язык кода. В конечном счёте их движение переросло в проектирование совершенно новых отношений между человеческим разумом и машинным интеллектом.
ЧАСТЬ I. ВИЗИОНЕРЫ (VISIONARIES)
Глава 1. Последнее средство Тома Хейлза (Tom Hales’s Last Resort)
В январе 1999 года в Институте перспективных исследований в Принстоне перед коллегами выступил математик Том Хейлз. Родившись в Сан-Антонио в 1958 году, Хейлз с детства поражал близких способностями к числам, окончил Стэнфорд и Принстон и стал профессором Мичиганского университета, работая в авторитетной области программы Лэнглендса. Однако в Принстоне он выступал по совершенно иному поводу: ему требовалось убедить математическое сообщество в том, что он решил проблему, остававшуюся непокорённой более 350 лет, — гипотезу Кеплера.
История гипотезы началась зимой 1611 года, когда астроном Иоганн Кеплер, гуляя по Карлову мосту в Праге, задумался о правильной шестиугольной форме снежинок. Интуиция подсказывала Кеплеру, что природа формирует структуры с наименьшими затратами пространства. Перенеся этот принцип на укладку шаров (например, пушечных ядер или апельсинов на лотке), Кеплер сформулировал гипотезу: наиболее плотной укладкой является пирамидальное расположение (с квадратным или шестиугольным основанием), при котором сферы занимают примерно 74% доступного объёма, а 26% остается пустым пространством.
Доказать это утверждение не удавалось веками. Карл Фридрих Гаусс в 1830-х годах доказал гипотезу для частного случая, когда шары строго расположены в узлах регулярной решётки. В 1900 году Давид Гильберт включил гипотезу Кеплера под номером 18 в свой знаменитый список 23 важнейших нерешённых проблем математики. В 1958 году Клод Амброз Роджерс доказал, что плотность не может превышать 78%, но дойти до кеплеровских 74% никто не мог.
Главная сложность гипотезы Кеплера заключалась в том, что она является задачей оптимизации с колоссальным количеством локальных оптимумов. Если высыпать теннисные мячи в тележку, они застрянут в устойчивом, но случайном положении со средней плотностью около 65%. Чтобы найти глобальный оптимум (74%), математикам потребовалось бы перебрать бесконечное или астрономически огромное число локально оптимальных конфигураций, что было невозможно традиционными методами.
В 1993 году Хейлз решил посвятить гипотезе Кеплера один полный год. Он взялся реализовать подход, намеченный в 1964 году венгерским математиком Ласло Феешем Тотом: свести проблему к проверке конечного числа конфигураций с помощью компьютеров. Вместе со своим аспирантом Сэмом Фергюсоном Хейлз разработал алгоритм, который сгруппировал расположение шаров и отссёк заведомо неоптимальные варианты, оставив для проверки 1762 особые конфигурации.
Поскольку уравнения конфигураций были нелинейными (содержали координаты $x, y, z$ в степенях для десятков шаров), запустить их напрямую на компьютере было невозможно — вычисления длились бы вечно. Хейлзу пришлось применить математическую хитрость: аппроксимировать нелинейные уравнения сложными линейными ограничениями. Это было похоже на измерение роста человека с помощью установки над его головой плоского потолка известной высоты: если потолок находится на высоте двух метров, а человек помещается под ним, его рост точно меньше двух метров.
На протяжении 1997 года Хейлз спал менее пяти часов в сутки, а остальные 17 часов проводил за подгонкой уравнений на кластере рабочих станций Sun Microsystems. К началу 1998 года у него осталось 50 наиболе спорных конфигураций. Он распечатал их схемы и развесил по стенам кабинета, как плакаты с разыскиваемыми преступниками. Проверив очередную конфигурацию на компьютере, он срывал со стены соответствующий плакат. К 4 июля 1998 года оставалась одна схема, а спустя пять дней расчётов компьютер выдал окончательный результат: плотность последней конфигурации строго меньше 74%.
Доказательство Хейлза состояло из 300 страниц рукописного текста и 3 гигабайт компьютерных вычислений. Он направил статью в самый престижный журнал поля — Annals of Mathematics. Редакция оказалась в тупике: вместо стандартных двух-трёх рецензентов журнал назначил команду из 12 экспертов. Прошел год, затем второй, затем третий, но эксперты выдавали один и тот же ответ: каждая отдельная проверенная часть выглядит корректной, но охватить целиком огромный массив кода и теоретических рассуждений они не в состоянии. В июне 2002 года один из главных рецензентов прямо написал редакторам, что отказывается читать свою часть, пока ему не гарантируют, что в остальных частях нет ошибок.
Прочитав книгу Сондерса Маклейна «Mathematics, Form and Function», Хейлз осознал, что традиционный социальный институт рецензирования доказательств сломался. 16 января 2003 года, получая премию Шовене в Балтиморе, Хейлз зачитал письмо из редакции Annals, в котором сообщалось, что рецензенты «исчерпали все силы» и не могут сертифицировать правильность доказательства. В ответ Хейлз заявил: «Компьютерные доказательства должны проверяться компьютерами».
Он объявил о старте проекта Flyspeck (от англ. flyspeck — детально разглядывать, а также квази-акроним Formal Proof of the Kepler Conjecture). Его целью был полный перевод доказательства гипотезы Кеплера в формальный код, понятный интерактивному доказателю теорем (ITP). Хейлз оценил объём работы в 20 человеко-лет. Он составил 286-страничный чертёж-план (blueprint) и выбрал в качестве рабочих систем ITP доказатели HOL Light и Isabelle.
Глава 2. Искатель истины (Truth Seeker)
Пока Том Хейлз начинал проект Flyspeck, в штате Вашингтон исследователь Microsoft Research Леонардо (Лео) де Моура двигался к созданию программы, которой было суждено изменить всю математику.
Де Моура родился в 1971 году в Рио-де-Жанейро в семье врачей. С детства его раздражали любые субъективные утверждения. Если взрослые называли башню из кубиков или картину «красивой», де Моура испытывал внутренний дискомфорт: как это можно доказать и проверить наверняка? Ему требовалась абсолютная, непререкаемая точность.
В 2001 году де Моура переехал в Калифорнию для работы в институте SRI (Stanford Research Institute) над проектом SAL (Symbolic Analysis Laboratory). Там он занимался поиском багов в софте с помощью верификации кода. Каждое действие программы образует трассу выполнения (execution trace), которую можно записать в виде математической формулы с сотнями и тысячами переменных. Поиск ошибки превращается в задачу проверки: существует ли такой набор условий, при котором формула принимает значение «истина», означающее переход программы в сбойное состояние.
В 2006 году руководить исследовательской группой Microsoft Том Болл пригласил де Моуру в Редмонд. Вместе с Николем Бьёрнером де Моура создал инструмент Z3 — автоматический доказатель теорем класса SMT (Satisfiability Modulo Theories). Инструмент показал феноменальную эффективность: перед выходом Windows 7 связка Z3 и внутреннего инструмента Sage нашла треть всех критических багов в системе, сэкономив Microsoft сотни миллионов долларов. Z3 из года в год выигрывал международные соревнования автодоказателей SMT-COMP.
Однако, достигнув вершины, 40-летний де Моура вновь почувствовал разочарование. Автоматические доказатели вроде Z3 имели неустранимые ограничения:
1. Они проверяли отдельные трассы кода, но не могли дать глобальную гарантию того, что программа корректна при любых вводных данных.
2. Они страдали от «нестабильности доказательств» (proof instability): незначительное изменение одной строки в коде могло привести к тому, что Z3 зависал навсегда, не в силах повторить успешное доказательство.
3. Класс задач, решаемых Z3, был алгоритмически неразрешим (undecidable).
В июле 2013 года де Моура пришел к Тому Боллу и заявил, что оставляет Z3, чтобы с нуля создать новый интерактивный доказатель теорем (ITP) — программу, в которой человек и машина шаг за шагом конструируют доказательства вместе.
Идея де Моуры опиралась на длительную интеллектуальную традицию формализации мысли:
- Аристотель (IV в. до н. э.) создал силлогизмы — логические схемы, где из двух истинных посылок с необходимостью следует вывод (например: Сократ — человек; все люди смертны; следовательно, Сократ смертен).
- Рамон Луллий (XIII в.) придумал механическое устройство из концентрических вращающихся колес с 16 божественными атрибутами для комбинирования логических истин.
- Готфрид Лейбниц (XVII в.) мечтал о универсальном символическом языке (characteristica universalis), комбинировании понятий (ars combinatoria) и вычислителе рассуждений (calculus ratiocinator), чтобы люди при спорах могли просто сказать: «Давайте посчитаем!».
- Евклид свыше 2000 лет назад дал строгое логическое доказательство иррациональности \(\sqrt{2}\).
- В конце XIX — начале XX века кризис оснований математики привёл к созданию теории множеств Цермело — Френкеля с аксиомой выбора (ZFC), а также теории типов в грандиозном труде Бертрана Рассела и Альфреда Норта Уайтхеда Principia Mathematica.
- Курт Гёдель в 1931 году доказал теоремы о неполноте, указав границы формальных систем, но одновременно подчеркнув потенциал механической проверки математики.
С появлением компьютеров возникли алгоритмы проверки выполнимости формул (SAT-сольверы). В 2016 году SAT-сольвер решил проблему пифагоровых троек, обработав более триллиона вариантов.
Фундаментальным прорывом XX века стало соответствие Карри — Говарда (открытое Хаскеллом Карри в 1930-х и формализованное Уильямом Говардом в 1960-х). Оно установило прямую эквивалентность между математическими доказательствами и компьютерными программами. Выражение типа данных в программе соответствует логической формуле, а исполняемая программа — доказательству этой формулы. Таким образом, любой инструмент, созданный для верификации программного обеспечения, по своей природе идеально подходит для написания и проверки математических теорем.
Глава 3. Скромноеначало Lean (A Lean Beginning)
К 2013 году в мире существовало несколько интерактивных доказателей теорем (ITP): Coq (созданный во Франции в 1989 г.), Agda (1999 г.), а также Isabelle (1986 г.) и HOL Light (1991 г.), которые Том Хейлз использовал в проекте Flyspeck. Однако ни один из них не получил признания среди практикующих математиков. Математики считали их громоздкими инструментами, созданными информатиками для своих специфических задач.
Де Моуру интересовала полезность программы. Любой ITP состоит из двух частей: логического фундамента (logical foundation) и микроскопической программы проверки — ядра (kernel). Ядро проверяет правильность шагов доказательства. Чтобы пользователи могли доверять ITP, де Моура принял ключевое архитектурное решение: сделать ядро Lean предельно малым и лаконичным. Тогда любой пользователь мог бы легко написать собственное ядро на любом языке программирования для перепроверки результатов, исключая риск багов в самой системе.
Летом 2013 года в столовой Microsoft де Моура пообщался с легендой мира формализации Жоржем Гонтье, который в 2005 году с помощью Coq формализовал доказательство известной теоремы о четырёх красках. Гонтье убедил де Моуру, что наилучшим фундаментом для ITP является зависимая теория типов (Dependent Type Theory).
В этот момент траектория де Моуры пересеклась с Джереми Авигадом. Авигад родился в Нью-Йорке в 1968 году, окончил Гарвард (где слушал лекции Тома Хейлза), защитил докторскую диссертацию в Беркли и стал профессором математики и философии в Университете Карнеги — Меллона. В 2005 году Авигад формализовал в Isabelle доказательство теоремы о распределении простых чисел. Он давно мечтал сделать ITP удобными для рядовых математиков.
В мае 2012 года Авигад и его молодой коллега Грант Пассмор задумали внедрить функции формального доказательства в популярную среди математиков открытую систему SageMath. За консультацией по внедрению Z3 они обратились к де Моуре. Между Авигадом и де Моурой началась ночная переписка по электронной почте, напоминавшая дуэль двух изощрённых юристов. Авигад настаивал, что простая теория типов (используемая в HOL Light) заставляет математика заново конструировать очевидные эквивалентные объекты, и требовал зависимых типов. Де Моура отстаивал минимализм ядра.
10 июля 2013 года де Моура огорошил Авигада сообщением: он полностью оставляет Z3 и начинает писать абсолютно новый open-source доказатель. 21 июля де Моура сообщил, что сдаётся под аргументами Авигада и Гонтье: в основе новой системы будут зависимые типы. В том же письме он впервые озвучил название проекта — Lean (англ. строгий, экономный, без излишеств).
В отличие от Coq, базировавшегося на конструктивной математике (где объект существует, только если вычислен алгоритм его построения), де Моура заложил в Lean классическую математику. Он добавил аксиому закона исключённого третьего и аксиому экстенсиональности функций.
Эволюция ранних версий Lean развивалась стремительно:
- Lean 0.1 (конец 2013 — начало 2014 г.): сырой прототип без графического интерфейса. Авигад запускал его из командной строки. 11 февраля 2014 года Авигад отправил де Моуре письмо с темой «Euclid vindicated», в котором содержалось первое историческое доказательство, принятое Lean — евклидово доказательство бесконечности простых чисел. Впрочем, сам де Моура на свадьбе Пассмора в январе 2014 года откровенно назвал Lean 0.1 «куском дерьма» и ушёл в «кодинговую пещеру» переписывать всё с нуля.
- Lean 2 (2014–2015 гг.): получил поддержку индуктивных типов данных, интерактивный двухпанельный интерфейс (слева — редактор кода, справа — окно состояния целей, выдающее заветную фразу «no goals», когда доказательство завершено) и язык скриптов-помощников — тактик (tactics). Тактики автоматически закрывали очевидные рутинные шаги (например, перестановку слагаемых \(a+b+c = b+c+a\)).
20 марта 2015 года де Моура приехал в Университет Карнеги — Меллона с демонстрацией Lean 2. В аудитории среди студентов сидел высокий подтянутый гость — Том Хейлз, пришедший посмотреть на человека, создавшего новый инструмент для математики. Официальный публичный релиз Lean 2 состоялся в августе 2015 года на конференции CADE в Берлине.
ЧАСТЬ II. РАННИЕ ПОСЛЕДОВАТЕЛИ (EARLY ADOPTERS)
Глава 4. Создание Mathlib (Building Mathlib)
После официального релиза Lean 2 на конференции CADE в Берлине в августе 2015 года программа впервые вышла за пределы узкого круга коллег Лео де Моуры. Сам де Моура выложил исходный код системы в свободный доступ на GitHub, но тут же вернулся в Microsoft Research, чтобы начать работу над Lean 3. Он считал Lean 2 лишь несовершенной площадкой для экспериментов, где практически всё приходилось делать вручную, и планировал создать идеальный инструмент верификации программного обеспечения.
Однако Джереми Авигад увидел в релизе реализацию своей давней мечты: возможность построить интерактивный доказатель теорем, изначально ориентированный на нужды научных математиков. Главной преградой было то, что «из коробки» Lean совершенно не знал математики. Если не считать нескольких базовых аксиом и логических правил, программа знала о предмете меньше, чем восьмиклассник. В отличие от обычного математика, работающего с мелком у доски, пользователь Lean не мог просто призвать на помощь свойства простых чисел или теорию групп — всё это сначала нужно было с нуля объяснить компьютеру.
Авигад вместе со своими студентами Флорисом ван Дорном и Робом Льюисом приступил к заполнению пустых полок. Им приходилось принимать фундаментальные архитектурные решения, которые зафиксировали стиль записи Lean на годы вперёд. Например, вместо традиционной для математиков записи функций $f(x)$ в Lean скобки оказались лишними, и стандартным стилем стало f x. Когда Авигад формализовывал гомоморфизм групп, ему пришлось выбирать: расщепить ли определение на два отдельных типа (тип функции и тип свойства) или упаковать их в один. После долгих консультаций с де Моурой они выбрали вариант с двумя типами. Каждая готовая конструкция отправлялась в виде пулл-реквеста (pull request) на GitHub. За 2015–2016 годы де Моура одобрил более 1000 коммитов в библиотеку Lean 2, а Авигад и его студенты добавили ещё 600.
Осенью 2015 года в аспирантуру Авигада поступает необычный студент — Марио Карнейро. Окончив Университет штата Огайо с тройной специальностью (физика, математика и информатика), Карнейро уже внёс колоссальный вклад в проект Metamath — низкоуровневый доказатель, в котором он вручную формализовал около 10 000 доказательств аксиоматической теории множеств. В июле 2015 года на конференции в Вашингтоне Лео де Моура и его интерн Даниэль Сельсам услышали доклад Карнейро. Поражённые его гениальностью, они вели себя как скауты НБА, нашедшие самородок на уличной площадке. В рекомендательном письме де Моура назвал Карнейро «одним из 0,1% лучших студентов, которых он когда-либо встречал».
Летом 2016 года в Lean 3 с помощью Сельсама был внедрён специальный язык метапрограммирования, позволявший пользователям писать собственные тактики — макросы, автоматизирующие рутинные логические шаги.
Однако между де Моурой и математическим сообществом нарастало напряжение. Для де Моуры поддержка пользователей была тяжёлой обузой, отвлекавшей от разработки ядра. Когда австралийский математик Ким Моррисон начал формализовать в Lean сверхабстрактную теорию категорий, де Моура жаловался Авигаду: «Из всех вещей на свете, неужели это обязательно должна быть теория категорий?». Ситуация обострилась, когда французский исследователь Армаэль Генео попытался верифицировать язык программирования, что потребовало небольшого изменения в кодировании массивов. Это изменение внезапно «сломало» код, ранее загруженный в библиотеку Марио Карнейро. Для де Моуры это был кошмар: безупречная основа программы оказалась замусорена полуготовым математическим кодом.
Кульминация конфликта произошла летом 2017 года на шестинедельной конференции Big Proof в Институте Ньютона в Кембридже. Там Том Хейлз представил проект Formal Abstracts (создание формальных цифровых аннотаций к ключевым математическим статьям) и объявил, что выберет Lean в качестве основного языка. На конференции Карнейро выступил с радикальным предложением: математическая библиотека Lean должна строиться по модели Википедии — стать полностью открытой для краудсорсинга со всего мира.
Де Моура и Авигад сначала посчитали идею хаосом, но Карнейро пообещал взять всю рутину по проверке кода и обучению новичков на себя. В середине июля 2017 года де Моура, Авигад и Карнейро заключили соглашение: математическая библиотека отделяется от ядра программы в самостоятельный репозиторий под названием Mathlib. Де Моура полностью умыл руки от содержимого Mathlib, оставив за собой лишь ядро (corelib) и утилиты для верификации софта. Он очистил Slack-каналы от пользователей, задававших базовые вопросы, и сосредоточился на собственной исследовательской программе.
Глава 5. Формальный кризис (A Formal Crisis)
В июле 2017 года 48-летний профессор Имперского колледжа Лондона Кевин Баззард сидел в садовом сарае в Северном Лондоне и смотрел трансляцию конференции Big Proof. В молодости Баззард был вундеркиндом: победил на Международной математической олимпиаде (IMO) в Гаване в 1987 году с абсолютным результатом (42 балла из 42), защитил диссертацию в Кембридже и получил бессрочную профессуру в области \(p\)-адической программы Лэнглендса. Однако после рождения троих детей его научная активность снизилась. Чтобы занять гиперактивный ум в редкие свободные минуты, он увлёкся видеоиграми (включая The Legend of Zelda) и настольной игрой «Точки и квадраты» (Dots and Boxes), став в ней неофициальным чемпионом мира.
Вернувшись к чтению свежих статей в 2016 году, Баззард испытал глубокий шок. Он обнаружил, что современная математика переполнена неточностями, логическими пробелами и снобизмом. Молодёжь строила свои работы на вершине фундаментальных трудов гениального Петера Шольце (создателя перфектоидных пространств), но делала это настолько небрежно, что Баззард опасался краха всей области. Эксперты на его замечания лишь отмахивались: «Ну, в целом-то всё верно!». Аналогичные опасения выражал и лауреат Филдсовской премии Владимир Воеводский, обнаружвший критическую ошибку в своей собственной давно признанной статье.
Слушая на трансляции доклад Тома Хейлза, Баззард был поражён. Хейлз показал слайд с 30 современными математическими определениями, которые он планировал формализовать в Lean. Баззард ранее считал, что доказатели теорем способны лишь на перебор «простых объектов» (как в теореме о четырёх красках), но списки Хейлза содержали глубокие понятия из высшей алгебры.
Баззард мгновенно написали Хейлзу и Авигаду, скачал учебник Авигада «Theorem Proving in Lean» и погрузился в изучение языка. Осенью 2017 года он решил провести эксперимент: заставить первокурсников Имперского колледжа сдавать еженедельные домашние задания на Lean.
Первое же базовое задание обернулось откровением. Баззард задал вопрос: «Пусть \(x\) — реальное число. Верно ли, что если \(x^2 - 3x + 2 = 0\), то \(x = 1\)?». Для человека ответ «очевидно ложно», так как \(x\) может быть равен 2. Но когда Баззард перевёл задачу на Lean, программа ответила: «Зависит от \(x\)» (ведь при \(x=1\) импликация истинна). Баззард осознал: человеческий язык математики невероятно неточен, а Lean заставляет быть безупречно строгим.
Студенты-слабаки невзлюбили Lean — для них это выглядело как попытка учить математику на чужом языке программирования. Тогда Баззард сменил тактику: он создал кружок по четвергам — Xena Project. Его амбициозной целью стала формализация всего курса бакалавриата по математике.
Однако Баззард понимал, что бакалаврской программой коллег-профессоров не удивить. В марте 2018 года вместе с талантливым студентом Кенни Лау он формализовал схемы (schemes) — сложнейший объект алгебраической геометрии, введенный Александром Гротендиком в 1960 году. Когда Баззард гордо рассказал об этом коллегам у туалета на 6-м этаже факультета, профессор Паоло Касчини усмехнулся: «Кевин, я знал, что такое схема, ещё когда был аспирантом».
Баззард понял: чтобы пробить стену скепсиса, нужно формализовать не просто «старую математику», а самый модный и сложный объект XXI века — перфектоидные пространства Петера Шольце.
Глава 6. Трюк с перфектоидными пространствами (The Perfect(oid) Stunt)
Летом 2017 года Патрик Массо, профессор симплектической геометрии из Орсе (Университет Париж-Сакле), столкнулся с нудной и громоздкой вычислительной проверкой в диссертации своего студента Фабио Жиронеллы. Желая автоматизировать рутину, Массо зашёл в чат Lean на платформе Gitter. Там он познакомился с Баззардом. Хотя оба работали в разных областях, оба занимались «модной математикой» (fashionable mathematics).
Массо и Баззард быстро осознали: в августе 2018 года на Международном конгрессе математиков (ICM) в Рио-де-Жанейро 30-летний Петер Шольце гарантированно получит Филдсовскую премию. Если им удастся формализовать его перфектоидные пространства в Lean, это станет грандиозным маркетинговым прорывом для всей системы. Перфектоидные пространства — это фракталоподобные структуры, связывающие алгебру, топологию и теорию чисел. Ничего подобного по уровню абстракции в доказатели теорем никогда не закладывалось.
Вскоре к их дуэту присоединился Йохан Коммелин, 28-летний нидерландский постдок из Университета Фрайбурга. Они разделили обязанности: Баззард и Коммелин взяли на себя алгебру, а Массо — топологию. Для проверки топологических оснований Массо использовал 29-томный труд французского коллектива «Николя Бурбаки». При переводе Массо даже нашёл пару мелких ошибок, пропущенных легендарными французами. Складывавшаяся культура Mathlib требовала максимальной абстрактности и универсальности кодирования каждого определения. Чтобы успевать за потоком изменений, Марио Карнейро спал с компьютером у кровати, настроенным громко пищать при любом упоминании его имени в Zulip.
Пока математики штурмовали перфектоидные пространства, Лео де Моуру окончательно допекли бесконечные споры на GitHub и требования исправить мелкие баги. В апреле 2018 года де Моура официально объявил, что версия Lean 3.4.0 станет последней, а разработку Lean 4 он переносит в закрытый, приватный репозиторий. На вопрос в чате, почему проект закрывается от публики, де Моура коротко ответил: «Я хочу работать в тишине». Авигаду он и вовсе признался: «С моей точки зрения, они — кучка избалованных детей».
Тем не менее математики не остановились. В сентябре 2018 года к 50-летию Кевина Баззарда участники чата Zulip сделали ему подарок: формализовали в Mathlib функции синуса, косинуса и число \(\pi\) (пошутив про праздничный «пирог»).
В январе 2019 года на конференции Lean Together в Амстердаме сообщество расширило состав хранителей (maintainers) Mathlib, включив туда Массо, Коммелина и Себастьена Гуэзеля (Баззарда намеренно исключили из-за его скандальной публичной риторики).
Для работы над перфектоидными пространствами математики активно использовали ключевое ключевое слово Lean — sorry. Оно позволяет поставить временную заглушку в месте непроверенного шага доказательства и двигаться дальше. Постепенно количество sorry сокращалось.
28 апреля 2019 года последний sorry был закрыт, и окно Lean выдало долгожданное сообщение: «no goals» / «Goals accomplished». Проект требовал более 12 000 строк кода. Массо создал интерактивную визуализацию: гигантскую «галактику» из 3000 узлов-теорем и 30 000 связей между ними, на вершине которой сияла звезда перфектоидных пространств.
11 мая 2019 года Баззард опубликовал триумфальный пост: «Lean способен справляться с истинно сложными объектами, представляющими реальный интерес для современной науки!». А за месяц до этого, 9 апреля 2019 года, математики с благословения де Моуры создали официальный комьюнити-форк Lean 3, полностью взяв управление кодом в свои руки.
Глава 7. Lean вместе (Lean Together)
Отделившись от математиков, де Моура получил долгожданный покой для разработки Lean 4. Его главным соратником стал молодой немецкий программист Себастьян Ульрих. Де Моура и Ульрих задумали революционный шаг: сделать Lean самоприменимым / раскручиваемым (self-hosting / bootstrapping). Если Lean 3 был написан на C++, а пользовательский код — на языке Lean, то Lean 4 должен был быть целиком написан на самом себе. Это сделало бы систему невероятно быстрой и гибкой.
В то же время комьюнити Mathlib продолжало бурное развитие. В мае 2020 года к сообществу присоединилась Хизер Макбет, молодой профессор Университета Фордхэм в Нью-Йорке. Она оценила академическую строгость рецензирования в Mathlib. Для новичков Баззард и его студент Мохаммад Педрамфар создали браузерную игру Natural Number Game, которая стала главный «входной дверью» в мир Lean для тысяч людей.
Начавшаяся весной 2020 года пандемия COVID-19 неожиданно дала движению мощный импульс: запертые на карантине математики массово устремились в чат Zulip.
В июле 2020 года Коммелин и Массо провели онлайн-воркшоп «Lean for the Curious Mathematician». Вместо ожидаемых 15 человек на него записались более 80 участников со всего мира, включая звезду французской математики Софи Морель. Во время воркшопа Морель нашла пробел в библиотеке линейной алгебры и лично отправила коммит № 3466 в Mathlib. За 2020 год число активных пользователей чата Zulip выросло с 1000 до более чем 3000 человек.
Параллельно в Microsoft Research развивалось ещё одно направление. Исследователь Даниэль Сельсам в 2019 году объявил о запуске IMO Grand Challenge. Его целью было создание искусственного интеллекта, способного завоевать золотую медаль на Международной математической олимпиаде. Сельсам планировал использовать обучение с подкреплением (reinforcement learning), где Lean выступал бы в роли непреложного арбитра, проверяющего корректность шагов ИИ.
На конференции Lean Together в январе 2021 года де Моура провел 2-часовую виртуальную презентацию Lean 4. Он открыто признал, что работа над новым движком — это «тяжёлая война и боль», но подвёл итог цитатой Джорджа Мартина: «Всех порадовать нельзя, поэтому нужно радовать себя». Де Моура осознал, что математики стали главными пользователями его творений, и был готов к новому витку эволюции Lean.
ЧАСТЬ III. ВДОХНОВИТЕЛИ (INFLUENCERS)
Глава 8. Математика высшей лиги (Big-League Math)
К ноябрю 2020 года немецкий математик Питер Шольце находился на самой вершине мирового математического олимпа. Завоевав Филдсовскую премию в 2018 году, он обладал репутацией гения, способного мгновенно находить суть и глубинные изъяны в самых запутанных работах. Именно Шольце вместе с Якобом Стикс в 2018 году опубликовал статью «Почему abc всё ещё остается гипотезой», указав на неустранимый логический разрыв в 500-страничном доказательстве Синити Мотидзуки.
Тем удивительнее было письмо, которое Шольце отправил Кевину Баззарду 28 ноября 2020 года. Письмо объёмом более шести страниц содержало просьбу о помощи: Шольце не был уверен в абсолютной корректности собственного доказательства, которое считал главным результатом своей карьеры.
Вместе со своим коллегой Дастином Клаузеном Шольце разрабатывал конденсированную математику (condensed mathematics) — новый фундамент для топологии, призванный заменить классические топологические пространства «конденсированными множествами». Чтобы доказать жизнеспособность теории, им требовалось перенести на новые объекты методы вещественного функционального анализа. Летом 2019 года Шольце непрерывно удерживал всю цепочку рассуждений в голове. Однажды в четверг доказательство почти сложилось, и Шольце отправился отмечать успех в бар Бонна с коллегой Ойгеном Хеллманном. На следующий день, страдая от сильнейшего похмелья, но опасаясь, что мысль ускользнет, Шольце совершил финальный математический прорыв.
Однако позже его охватили сомнения. Доказательство обладало чудовищной логической сложностью — цепочкой чередующихся кванторов вида $\forall \exists \forall \exists \forall \exists$, где нельзя было поменять местами ни одного звена. Помянув похмелье, сложность аргументации и собственную убедительность, перед которой ранее пасовали даже эксперты, Шольце спросил у Баззарда: есть ли шанс проверить это доказательство в Lean?
Для сообщества Lean это был шанс пройти главный тест: формализовать сложное доказательство сложного объекта. Йохан Коммелин взял руководство проектом на себя, получив предварительное подтверждение от Рейда Бартона, что в Mathlib уже есть базовые кирпичики. Чтобы не рисковать репутацией ради безымянной проверки, Коммелин попросил Шольце публично подтвердить важность задачи. 5 декабря 2020 года Шольце опубликовал в блоге Баззарда пост «Liquid Tensor Experiment» (название отсылало к «жидким векторным пространствам» и любимой рок-группе Liquid Tension Experiment).
Проект состоял из двух частей:
1. Теорема 9.4 («крутая стена») — техническое доказательство, в котором сомневался Шольце.
2. Импликация 9.4 $\to$ 9.1 («высокое плато») — вывод главного результата condensed-математики из Теоремы 9.4.
Коммелин штурмовал Теорему 9.4, обсуждая каждый шаг с Шольце в Zulip. В один из моментов Коммелин обнаружил, что Шольце использовал вариант свойства «точности комплексов», автоматически посчитав, что для него сохраняются все классические свойства. Шольце признался, что в этот момент «покрылся холодным потом», но быстро смог ликвидировать брешь. В процессе верификации Коммелин и Адам Топаз создали набор тест-кейсов («модульных тестов» / «абдуктивных рассуждений»), чтобы доказать Шольце, что формальные определения в Lean строго соответствуют математическому смыслу.
28 мая 2021 года, за считанные минуты до семейной поездки, Коммелин задел последний sorry. Lean подтвердил: Теорема 9.4 верна! Коэффициент де Брёйна (отношение длины формального кода к тексту статьи) составил всего 20 — феноменальный результат.
Вторая часть (связка 9.4 и 9.1) занимала в рукописи Шольце всего 5 строк, но потребовала формализации всей высшей теории категорий, когомологий и пучков. Коммелин расставил в чертеже проекта заглушки sorry как сигнальные ракеты, приглашая математиков со всего мира подключаться к работе. В итоге 28 исследователей объединили усилия. 15 июля 2022 года на конференции в Род-Айленде Коммелин объявил: проект полностью завершён, граф зависимостей стал абсолютно зелёным. Этот успех окончательно примирил Лео де Моуру с математическим сообществом.
Глава 9. Главный вызов для ИИ (The AI Grand Challenge)
В конце 2021 года исследователь лаборатории DeepMind Тома Юбер пересматривал лекцию Кевина Баззарда «Будущее математики» 2019 года. Вводное слово к лекции давал Лео де Моура, который рассказал о проекте своего коллеги Даниэля Сельсама IMO Grand Challenge — попытке создать ИИ, способный завоевать золотую медаль на Международной математической олимпиаде. Де Моура подчеркнул, что если шахматы и го — это игры с конечным пространством ходов, то математика — это «бесконечное пространство действий с магическими человеческими ходами».
Юбер идеально подходил для этого вызова. Чемпион Франции по го и магистр математического финансирования Стэнфорда, он работал в DeepMind с 2015 года. Он был одним из ключевых разработчиков нейросетей AlphaGo, AlphaGo Zero и AlphaZero, разгромивших лучших игроков мира в го, шахматы и сёги с помощью обучения с подкреплением (reinforcement learning).
После выхода ChatGPT в ноябре 2022 года мир заговорил о больших языковых моделях (LLM). Однако математики быстро обнаружили, что обычные LLM склоны к галлюцинациям и легко ошибаются в элементарной арифметике и логике. Команда Юбера в DeepMind осознала: истинный прорыв лежит в гибридном подходе — объединении гибкости LLM и безупречного контроля правильности шагов со стороны Lean. Так началась разработка AlphaProof.
Для обучения AlphaProof требовался огромный массив данных. К 2023 году библиотека Mathlib разрослась с 213 000 до более чем 1 миллиона строк кода. В июле 2023 года сообщество завершило титанический перенос всей библиотеки с Lean 3 на Lean 4 с помощью инструмента Mathport, созданного Марио Карнейро.
Чтобы обучить AlphaProof, DeepMind требовалось превратить миллионы школьных текстовых задач в код Lean (автоформализация). LLM успешно научилась переводить в код до 80% задач по алгебре и теории чисел. Однако комбинаторные задачи, написанные в виде сюжетов (например, про «улитку Турбо», ползающую по полю с монстрами), давались автоформализации с трудом, так как требовали построения сложнейших абстракций.
Сгенерировав 10 миллионов задач в формате Lean, DeepMind запустила непрерывный цикл обучения с подкреплением. Системным «литражом» стал разбор задачи №1 с IMO 2019 года, которую AlphaProof успешно решил в начале 2024 года.
В июле 2024 года на Олимпиаде в Бате (Великобритания) AlphaProof неофициально вступил в соревнование. Задачу по геометрии (№4) за 19 секунд решила специализированная программа AlphaGeometry. AlphaProof безупречно справился с задачами №1, №2 и сложнейшей алгебраической задачей №6 (о так называемых «акваэсулианских функциях»). Единственной непокорённой вершиной стала задача №5 про улитку Турбо, где система получила 0 баллов из-за сложности перевода сюжета в сетку множеств Lean.
С результатом 28 баллов из 42 AlphaProof завоевал серебряную медаль IMO, отставая всего на 1 балл от золотого порога. Это стало крупнейшей демонстрацией возможностей машинного мышления в истории.
Глава 10. Команда Терри Тао (Team Terry Tao)
Терренс (Терри) Тао всегда отличался неординарным масштабом мышления. Вундеркинд из Австралии, который в 7 лет учил матанализ, а в 10 стал самым молодым призёром IMO в истории, Тао к 24 годам стал профессором UCLA, а в 2006 году получил Филдсовскую премию. В 2009 году он поддержал инициативу Тима Гоуэрса Polymath Project — краудсорсинговое решение математических задач через комментарии в блогах.
В июле 2022 года Тао пригласил Кевина Баззарда и Джереми Авигада соорганизаторами воркшопа в институте IPAM. Баззард убедил Тао лично попробовать Lean.
9 октября 2023 года 48-летний Тао завел аккаунт в сети Mastodon и написал, что начинает проходить Natural Number Game. Затянутый азартом логической игры, Тао прошел её за один день (прибегая в сложных местах к помощи GPT-4 для обхода синтаксических затыков). На следующий день он выложил на arXiv доказательство неравенства Маклорена, а затем потратил месяц на то, чтобы перевести его на Lean 4. Code получился «корявым», но Тао официально вошел в комьюнити.
В ноябре 2023 года Тао вместе с Тимом Гоуэрсом, Беном Грином и Фредди Маннерсом доказал полиномиальную гипотезу Фреймана — Ружи (PFR). Тао предложил формализовать свежую статью.
В чате Zulip он запустил проект PFR. Студент Яэль Дилли создал интерактивный чертёж из 13 разделов. Тао разбил доказательство на микроскопические леммы по 5 строк кода и ввёл систему тикетов, распределяя задачи между десятками добровольцев со всего мира. Когда в конце проекта возникла задержка на банальном шаге (доказать, что множества {0}, {1} и {2, 3} не пересекаются), Тао написал 100 строк нудного кода проверки. Коммелин тут же подсказал ему встроенную тактику decide, закрывшую проблему в один клик. Проект PFR был полностью завершён за рекордные три недели!
В сентябре 2024 года Тао запустил еще более грандиозный эксперимент — Equational Theories. Он решился картографировать взаимосвязи между 4694 алгебраическими законами (что давало 22 миллиона логических импликаций). С помощью Python-скриптов, автоматических доказателей Z3, скриптов Lean и человеческой интуиции команда сократила 22 миллиона связей до нескольких десятков за пару месяцев. В процессе участники случайно открыли абсолютно новую математическую структуру — «когомологии магм» («математику с Марса»). Тао доказал: математика может быть экспериментальной и высокопроизводительной наукой.
Глава 11. Шагвбудущее Lean (Lean into the Future)
К 2024 году Лео де Моура достиг всего, о чём мечтал, хотя и не совсем так, как планировал. Lean стал главным стандартом цифровой математики.
В конце 2021 года де Моура и Даниэль Сельсам провели созвон с Сэмом Олтманом (OpenAI), который выразил восторг от Lean и заявил о желании решить проблемы тысячелетия. Вскоре Сельсам перешёл работать в OpenAI.
Летом 2022 года из-за сокращения бюджетов в Microsoft де Моуру стали подталкивать к переключению на генеративный ИИ вопреки развитию ядра Lean. В этот момент организация Convergent Research (основанная Эриком Шмидтом и Кеном Гриффином) предложила де Моуре создать независимую некоммерческую организацию — Lean FRO (Focused Research Organization). Чтобы не терять в доходе, де Моура в марте 2023 года перешел на верхнюю позицию в Amazon Web Services (AWS), а в Lean FRO стал волонтёром-CEO. Офис Lean FRO нанял около 20 штатных инженеров для поддержки ядра и инфраструктуры Mathlib.
Параллельно Джереми Авигад получил грант на 20 миллионов долларов от криптопредпринимателя Чарльза Хоскинсона на создание Центра формальной математики в Карнеги — Меллоне. Авигад занялся разработкой супер-автоматизации — инструмента Lean-Sledgehammer (включающего нейросети, сольвер Duper и Lean-auto), позволяющего закрывать огромные куски доказательств одной кнопкой.
Педагоги разработали адаптации системы:
- Хизер Макбет написала интерактивный учебник The Mechanics of Proof, заблокировав слишком мощные тактики, чтобы студенты учились рассуждать по шагам.
- Патрик Массо создал Verbose Lean, позволяющий писать код на естественном английском или французском языке.
- Алекс Конторович организовал воркшоп «Lean for Mathematicians» (убрав слово «любопытных», так как Lean стал мейнстримом).
К 2025 году Кевин Баззард отошел от публичной роли «рок-звезды от математики» и передачи сцены Терри Тао. Получив грант в 1 миллион фунтов стерлингов, Баззард вернулся к работе руками: он начал масштабный проект по полной формализации легендарного доказательства Последней теоремы Ферма, сделанного Эндрю Уайлсом в 1994 году.
Индустрия ИИ окончательно сделала Lean своим главным звеном. Стартап Harmonic (созданный Владомт Теневым) с моделью Aristotle, Meta со своими «моделями мира», OpenAI и DeepMind используют Lean как единственную среду, способную дать 100% гарантию истинности и избавить ИИ от галлюцинаций.
9 января 2025 года в ресторане Aerlume в Сиэтле Лео де Моура, Джереми Авигад и их коллеги собрались за ужином, чтобы отпраздновать 57-летие Авигада. На следующий день де Моура и Авигад долго гуляли по набережной Сиэтла. Гуляя у Тихого океана, они вспоминали 12 лет совместного пути — от сырого Lean 0.1 до технологии, изменившей математику и искусственный интеллект навсегда. Лео де Моура признался, что впервые за всю жизнь смотрит в будущее с абсолютным оптимизмом.
Summarizator — это Telegram-канал, где мы собираем саммари самых актуальных и захватывающих книг об ИИ, технологиях, саморазвитии и культовой фантастике. Мы экономим ваше время, помогая быстро погружаться в новые идеи и находить инсайты, которые могут изменить ваш взгляд на мир. 📢 Присоединяйтесь: https://t.me/summarizator