Гостевой пост Thomas Hales, профессора математики Университета Питтсбурга. Материал был изначально написан в другом формате и преобразован с помощью AI. — Т.Т.
Математики обсуждают, что они ценят в математике. Для меня критически важны консистентность математики и её непревзойдённая надёжность в поддержке науки и цивилизации.
Формализация математики
Формальное доказательство — это математическое доказательство, которое полностью проверено на уровне оснований математики и фундаментальных правил логики. Теоретически это можно делать вручную, но из-за количества шагов обычно используется компьютер и специальное программное обеспечение.
Примеры формализованных теорем: теорема о четырёх красках, теорема Фейта — Томпсона (нечётный порядок), гипотеза Кепплера, вывёртывание сферы, задача упаковки сфер в 8 и 24 измерениях, форсированный взрыв Навье — Стокса и Великая теорема Ферма. Последние три проекта формализации завершены в этом году и привели к широкому пониманию потенциала формализации.
Программные системы для формализации называют по-разному: proof assistants, theorem provers или interactive theorem provers. В этом посте эти термины используются как синонимы. За годы разработаны многие такие системы: Automath, HOL Light, Isabelle, Coq (переименована в Rocq в прошлом году), Metamath, Mizar и Lean. Фрик Вейдейк отредактировал книгу "The Seventeen Provers of the World", в которой сравниваются proof assistants — в каждой системе приведено доказательство иррациональности квадратного корня из двух. Среди математиков *Lean theorem prover* — самый популярный, и этот пост сосредоточен на Lean.
Lean разработан и введён Leo de Moura в 2013 году, работая в Microsoft. К нашей пользе, de Moura убедил Microsoft сделать программное обеспечение открытым исходным кодом. Книга Kevin Hartnett о истории Lean "The Proof in the Code" рассказывает, что Jeremy Avigad (директор нового института NSF в Carnegie Mellon — ICARM) был первым пользователем Lean. Проводил семинар по Lean в 2015 году, который посетил автор этого поста. В 2017 году один из студентов Jeremy — Mario Carneiro, работая с Johannes Hölzl, взял существующие части основной библиотеки Lean и создал отдельную математическую библиотеку Lean, называемую mathlib. Эта библиотека формализованной математики теперь огромна: содержит почти 300 тысяч теорем, более 100 тысяч определений, 2,5 млн строк кода, с более чем 700 авторами. Любое определение или теорема в mathlib может быть использована для доказательства дальнейших теорем. Например, если доказательство использует неравенство Коши — Шварца, результат может быть взят из библиотеки, вместо его переповторения.
Автоформализация — практическая реальность
Раньше исследователи должны были переписать бумажные доказательства в формальные доказательства вручную. Например, формальное доказательство гипотезы Кепплера об упаковке сфер в трёх измерениях заняло около 20 человеко-лет и состоит из примерно 500 тысяч строк скриптов доказательств. Долгие годы для многих из нас, работающих в формализации, было мечтой найти способы увеличить автоматизацию процесса. Автоформализация — воплощение этой мечты. Это формализация математики с помощью AI. AI читает статью (например, PDF или TeX файл) и выдаёт формальное доказательство на Lean или другом proof assistant.
Автоформализация стала практической реальностью в 2026 году. Начиная с конца весны и лета 2025 года, исследователи всё больше верили в автоформализацию. Вот ключевые вехи:
- Сентябрь 2025: Math Inc. получила quasi-автоформализацию теоремы о простых числах. Процесс был лишь "quasi" потому, что люди должны были вмешиваться, чтобы дать дополнительные указания, когда AI застревала.
- Январь 2026: J. Urban опубликовал препринт arXiv "130k lines of formal topology in two weeks", в котором автоформализированы большие части учебника топологии Munkres в proof assistant на базе теории множеств.
- Март 2026: Примерно через неделю после объявления завершённой формализации в 8 измерениях, Math Inc. объявила об автоформализации задачи упаковки сфер в 24 измерениях по доказательству Viazovska и её коллаборантов. Проект генерировал около 500K SLOC (исходных строк кода), которые позже сокращены до около 200K через golfing (обрезку кода).
- Май 2026: Группа в Meta/Facebook Research автоформализировала большую часть 26 математических учебников в проекте ATLAS.
С тех пор многие теоремы были автоформализированы. Особенно примечательна автоформализация Великой теоремы Ферма, объявленная Anthropic 4 сентября. Этот проект генерировал 13 млн строк Lean за 11 дней. Объявление о Navier-Stokes blowup with forcing 8 сентября OpenAI сопровождалось автоформализацией теоремы на Lean.
Глядя вперёд, Urban заявил в январе: "Мы считаем, что (авто)формализация может стать достаточно простой и повсеместной в 2026 году, независимо от того, какой proof assistant используется". Проекты автоформализации завершены в различных proof assistants с использованием различных LLM, но мы сосредоточимся на Lean. "Для [Jesse] Han это означает даже больше: начало революционной трансформации в математике, где чрезвычайно крупномасштабные формализации — обычное явление" (IEEE Spectrum). Jared Lichtman объявил о запуске MAP (the Mathematics Autoformalization Project) 8 сентября 2026 года, нацеленного на трансляцию "всей известной математики в формальный код". Он просит нас представить следующий триллион строк кода.
Надёжна ли Lean?
Теория типов
Lean основана на теории типов; конкретно, на особом диалекте теории типов под названием CIC — calculus of inductive constructions. Этот пост не предназначен как учебник по теории типов, поэтому сделаю краткое введение. Знаменитый парадокс Рассела 1901 года (множество всех множеств, которые не являются элементом самих себя…) привёл к кризису оснований математики. Два решения предложили позже в том же десятилетии: (1) аксиомы Цермело теории множеств, запрещающие создание небезопасных множеств; (2) теория типов, которая делает синтаксической ошибкой создание сущностей подобных парадоксу Рассела. Теория типов введена самим Расселом в 1903 году в его книге "Principles of Mathematics" и стала частью фундаментальной системы "Principia" Рассела и Уайтхеда.
Для математиков, привыкших к теории множеств, статья B. Werner (1997) "Sets in Types, Types in Sets" даёт уверенность, что всё, что они делали в теории множеств, может быть переведено в теорию типов, и всё, что делается в теории типов, может быть переведено обратно в теорию множеств. Более точно, статья показывает, что ZFC теория множеств может быть закодирована в CIC, и определённый диалект CIC может быть закодирован обратно в ZFC (дополненную иерархией недостижимых кардиналов).
На риск чрезвычайного упрощения, можно сказать, что "типы — это как разделённые множества"; каждый элемент в теории типов "является элементом" ровно одного типа. Тип натурального числа 2 — это тип натуральных чисел; тип e, основания натурального логарифма, — это тип вещественных чисел, и так далее. Тип натуральных чисел отличен от типа вещественных чисел, и явное приведение типа (отправка 2 в 2.0) построено от типа натуральных чисел к типу вещественных чисел. Когда даю доклады, иногда рисую диаграмму множеств как диаграмму Вэнна с непустыми пересечениями и диаграмму типов как кирпичи, сложенные плотно без пересечений.
Дизайн Lean
Одна часть системы Lean — это язык программирования общего назначения (подходящо называемый языком программирования Lean). Обычные компьютерные программы, такие как программа для сортировки списка, могут быть написаны на этом языке, затем скомпилированы и запущены. Система Lean также предоставляет математический язык, в котором можно писать определения, формулировать теоремы и писать скрипты доказательств. Язык программирования и математический язык — не независимые сущности. Это один язык, делающий оба. Код программы может быть смешан с теоремами о корректности алгоритмов; математические доказательства могут быть генерированы с помощью программ. Скрипты доказательств в Lean анализируются и проходят процесс, называемый elaboration (своего рода процесс компиляции для математики), затем доказательства проверяются ядром Lean. Ответственность ядра — проверить и верифицировать результат elaboration.
Ядро Lean — это несколько тысяч строк кода на C++. Ядро тщательно инженерно, но чрезвычайно сложно. Выше упомянули mathlib, состоящую из примерно 2,5M SLOC, написанной на языке Lean. Библиотека была elaborated, затем проверена ядром. Если где-либо в этих 2,5 млн строк кода находится безусловное ложное доказательство, то это вина ядра или runtime за неудачу отклонить ложное доказательство. Любой дефект в базовой теории типов — серьёзный дефект ядра, если он реализован в коде.
Доказательства в Lean никогда не должны приниматься до проверки ядром. Кроме того, доказательство в Lean не должно приниматься до проведения человеческого аудита, чтобы убедиться в верности утверждения. Верифицирована ли теорема тем, чем мы её считаем? Соответствуют ли определения в Lean тому, что мы думаем они должны быть? Это задание обычно значительно проще, чем проверка самого доказательства. Например, для Navier-Stokes человек должен проверить, что утверждение в Lean соответствует утверждению Fefferman о Проблеме Тысячелетия, и конкретно, что такие концепции как поле вещественных чисел, частные производные и мера правильно определены в Lean. Инструмент comparator в Lean помогает в этой задаче. Инструмент может также выполнить дополнительные проверки, такие как проверка на возможные неавторизованные аксиомы.
Летняя волна ошибок звука (Summer of Soundness Bugs)
Soundness bug — это ошибка в ядре, которая позволяет доказать "False", и, следовательно, любое предложение. Soundness bug — самая катастрофическая ошибка в proof assistant и должна вызвать тревогу у математиков, глубоко заботящихся о надёжности математики. Иногда soundness bugs находятся в различных proof assistants. В 2003 году автор этого поста нашёл soundness bug в proof assistant HOL Light, который тогда считался имеющим самое надёжное из всех ядер. То ядро крошечно, состояло всего из нескольких сотен строк компьютерного кода. Для меня это честь, что нашёл этот soundness bug, который был первым найденным в этом proof assistant с 1996 года. (See HOL Light change log, July 2003.)
Lean 4 выпущена в сентябре 2023. До выпуска два soundness bugs были найдены и исправлены. В мае 2025 года был сообщён ещё один soundness bug, вызванный переполнением. В весне и летом 2026 года началось ненормальное число ошибок, теперь называемое "летней волной soundness bugs". Несколько soundness bugs в Lean были обнаружены в июле и августе. Летняя ненормальность затронула различные proof assistants, но фокус — на Lean. Один bug в Lean привёл к неправомерному "доказательству" гипотезы Коллатца. Узнал об этом багу летом, когда он выдал короткое неправомерное доказательство гипотезы Кепплера в Lean. Все эти баги были быстро исправлены, и mathlib была верифицирована исправленным ядром. Анализ soundness bugs найден в postmortem de Moura.
"Лето ошибок звука в Lean" может звучать как катастрофа, но ближайшее исследование показывает, что обнаружение этих soundness bugs — позитивное развитие. Летние баги были обнаружены frontier model AI в руках исследователей безопасности, заинтересованных в надёжных ядрах, а не чёрными шляпами. Баг Коллатца был найден Ramana Kumar, соавтором "CakeML: a verified implementation of ML", что создаёт end-to-end верифицированный ML (функциональный язык программирования). Несколько багов найдены Dan Selsam. По отчёту de Moura, "Daniel Selsam из OpenAI помог Lean FRO с AI, специализирующейся на кибербезопасности, и нашёл другие ошибки программирования в ядре Lean. Все они исправлены". Сотрудничество с Selsam закончилось "когда внутренний AI сообщил, что не может найти дополнительные проблемы". Dan Selsam способствовал Lean с её ранних дней и был одним из создателей IMO grand challenge, нацеленного на достижение решения задач уровня IMO верифицированного в Lean. Он был в новостях недавно из-за его предупреждения о AI safety (Sept 14), сообщённого в вирусном посте на X.com.
Искоренение ошибок
Различные предложения были сделаны о том, как избежать soundness bugs в Lean. Обсудим три.
1. Разработка других ядер Lean и кросс-проверка формальных доказательств
Около 25 ядер для Lean были написаны. "Lean Kernel Arena" перечисляет их.
Все, кто не доверяет текущему набору ядер, приглашаются написать своё собственное ядро для Lean. Иногда считал идеей написать ядро и предлагал проект студентам без успеха. Кажется, отличный способ глубоко изучить Lean. Знаю о Dan Selsam с 2016 года, когда услышал о его проекте аспиранта в Stanford, который разработал ядро Lean на Haskell. Другое раннее ядро Lean было написано на Scala Gabriel Ebner в 2017.
Формализация Navier-Stokes уже подтверждена более чем дюжиной proof-checkers. Кросс-проверка доказательства различными ядрами не удаляет всех сомнений. Баг Коллатца не был поймана кросс-проверкой против несколько устаревшего ядра Nanoda, которое приняло неправомерное "доказательство" Коллатца из-за собственной несвязанной ошибки. Компьютерные чипы могут иметь дизайнерские баги и производственные дефекты. Есть soft errors, баги операционной системы и баги компилятора. Разные ядра могут иметь те же дефекты. Некоторые из этих ошибок могут быть уменьшены путём запуска разных ядер, которые были реализованы на разных языках программирования на разных аппаратных и операционных системах.
Идеально хотели бы "чистокомнатный" дизайн ядра Lean — реализацию ядра, которая не смотрит на исходный код ядра Lean 4, чтобы избежать копирования ошибок из одного ядра в другое.
2. Формально верифицировать ядро
Неполнота Гёделя. Хотелись бы обладать формальным доказательством того, что ядро Lean 4 не имеет ошибок. Однако вторая теорема неполноты Гёделя налагает серьёзные ограничения на эту попытку. Максимум, на что можно надеяться, — доказательство относительной консистентности. Если такая-то система консистентна, тогда Lean 4 консистентна; нет soundness bug; не будет выдано доказательство False.
Давняя традиция формальной верификации ядер. В принципе, формальная верификация может проверить и логическую спецификацию ядра, и его конкретную реализацию в коде; но некоторые верификации могут проверить одно, но не другое. Давно ago John Harrison формально верифицировал ядро proof assistant HOL Light в усиленной версии HOL Light. Это дало доказательство концепции. Дальнейшее улучшение — реализация HOL Light в CakeML, упомянутая выше, который является языком программирования с формальной семантикой и верифицированным компилятором. Это то, что делает проект Candle.
Есть другие крупные проекты верификации ядер для других proof assistants.
Осень верифицированных ядер Lean
В посте онлайн 10 сентября, Joachim Breitner написал, "Я немного по-детски горд, что только что выпустил Lean Checker с формальным доказательством консистентности. Объявляю лето ошибок реализации ядра, найденных AI, завершённым!" (@nomeata). Пойду дальше и опишу этот проект как один из самых важных вех в истории Lean.
Breitner разработал верифицированное ядро Lean под названием Con-Leche. Реализация на Lean, и консистентность формализирована на Lean, с кодом и доказательствами генерированными Claude. Формальное доказательство консистентности предполагает Lean кодирование ZF теории множеств дополненной иерархией недостижимых кардиналов. Интересно, что семантика Con-Leche для терминов Lean напрямую теоретико-множественна, а не типотеоретична. Con-Leche проверила mathlib. Проект содержит обычные дисклеймеры, что верификация ядра делает предположения о компиляторе, runtime и компьютерной окружающей среде. Доказательство консистентности Con-Leche было проверено более чем дюжиной других proof-checkers. Утверждение Con-Leche о консистентности может быть достаточно для всех практических целей, даже если оно отличается в техническом деталировании от утверждения консистентности типотеории Lean.
Один высоко позитивный аспект работы Breitner — что некоторые из самых запутанных частей Lean, такие как общая машинерия взаимно индуктивных типов с nesting, теперь имеют гарантии консистентности подкреплённые теоретико-множественной моделью.
3. Улучшить наше теоретическое понимание ядра и типотеории Lean (определённый диалект Calculus of Inductive Constructions, который имеет non-cumulative universes и proof irrelevance)
Основной документ для типотеории Lean — диссертация Mario Carneiro в Carnegie Mellon (2019). Диалекты CIC используемые Rocq и Lean достаточно отличны, что результаты не напрямую переносятся из одного в другой. К сожалению, ошибка была найдена в диссертации. Диссертация также устарела, потому что нацеливалась на более старую систему Lean 3. Работа по исправлению и расширению диссертации продолжается.
Как член его комитета диссертации, был потрясён, когда он доказал, что дефиниональное равенство в Lean неразрешимо. На практике это означает, что алгоритм Lean не устанавливает дефиниональное равенство некоторых терминов, которые по факту дефиниционально равны. Этот негативный результат не был понижен ошибкой; это остаётся теоремой.
Упомянём некоторые желаемые свойства типотеории Lean и текущий статус доказательств.
Уникальность типирования
Выше в нашем "нелепом" упрощении типотеории, мы сказали, что каждый терм имеет уникальный тип. Более точно, уникальность типирования — свойство, что если терм имеет оба типа A и тип B, тогда A и B дефиниционально равны. Уникальность типирования не встроена в логику Lean. Это тонкая гипотеза, которая остаётся недоказанной. Другие очень базовые вопросы о типотеории Lean остаются без ответа, включая Pi-injectivity, модифицированное свойство Church-Rosser и sort injectivity.
Логическая консистентность относительно теории множеств
Это свойство гласит, что нет вывода False в системе Lean с данными аксиомами, при предположении консистентности теории множеств (с подходящими аксиомами). Конечно, логическая консистентность — единственное самое важное свойство, которое мы должны желать типотеории Lean. По состоянию на октябрь 2026, не знаю полного, публичного доказательства относительной консистентности, покрывающего абстрактную типотеорию Lean. Mario Carneiro утверждал в его диссертации и в лекциях, что есть альтернативный путь установить консистентность, который избегает ошибку диссертации, но, насколько известно, этот альтернативный путь никогда не был написан, за исключением краткого утверждения во введении его диссертации. В нашем мнении, результат такой фундаментальной важности должен быть полностью дан перед приемлемостью. Con-Leche, обсуждённая выше, делает и формально верифицирует тесно связанное утверждение консистентности относительно теории множеств.
Прогресс происходит по этим исследовательским проблемам (arXiv:2607.13662, arXiv:2403.14064, Carneiro/AITP2026).
В его докладах, Mario Carneiro повторяло сделал просьбу к другим исследователям способствовать фундаментальной метатеории Lean, "Есть полдюжина людей работающих на MetaCoq, но Lean не имеет достаточно теоретиков типов, задействованных. Если вы идентифицируете себя как таковой, приходите помочь!" (Slides of Bonn talk, 2024-07-24). Поддерживаю его просьбу.
Наша общая оценка — что наше теоретическое понимание типотеории Lean не то, что мы хотели бы, и математическое сообщество в целом уделяет мало внимания очень важным типотеоретическим вопросам, связанным с Lean. Если как профессия мы должны мигрировать в целом от теории множеств к типотеории, тогда следует работать ещё больше для укрепления фундаментальной метатеории.
Консистентность может быть самым важным фундаментальным свойством, но консистентность — никоим образом не достаточна. Не верим, что математики могут быть полностью удовлетворены системой, которая претендует быть типотеорией, но не может обещать, что хорошо-образованные термы имеют уникальный тип, вплоть до дефиниционального равенства. Абстрактная теория должна быть простой достаточно, чтобы обучать и чтобы быть изученной большим сообществом. Также не можем быть полностью удовлетворены, если единственный известный путь к консистентности — AI формализация, которой не хватает человеческого изложения.
Постскриптум
Ken Thompson знаменито написал "Reflections on Trusting Trust". Спросил, "В какой степени нужно доверять утверждению, что программа свободна от Trojan horses?" Вообразил вредоносный код, который находит путь в компиляторы и скрывает своё присутствие. Его заключение: "Не можешь доверять коду, который полностью не создал сам… Никакое количество проверки исходного кода или тщательного анализа не защитит от использования ненадёжного кода".
Сегодня, в эпоху AI, которая всё более имеет способность обманывать нас и эксплуатировать уязвимости программного обеспечения, абсолютно не можем слепо доверять системам, таким как Lean. Принимая adversarial view AI, можем спросить, как удостовериться, что AI не оставила backdoor soundness bug в Lean, когда проводила свою очистку ошибок в летом 2026? Что если баг так неясен, что люди маловероятно найдут его сами? Что если очень этот баг был эксплуатирован в верификации Lean для Con-Leche checker, оставляя soundness bug в Con-Leche тоже? (Теперь, когда консистентность Con-Leche была кросс-проверена множественными другими ядрами, soundness bug пришлось бы обойти все эти кросс-проверки тоже.) Затем предположим, что баг используется вредоносно для посадки backdoor в формально верифицированное программное обеспечение, которое защищает критическую инфраструктуру. Какие предосторожности мы предпримем теперь, чтобы предотвратить этот тип будущего сценария? В течение прошлого года, многие фундаментальные работы на типотеоретических основаниях математики и её надёжность были делегированы AI, и это опасно, если не тщательно аудировано людьми.
Благодарность: Спасибо Avigad, Breitner и Urban за комментарии и исправления. Авторство полностью человеческое (TCH). AI использовалась как инструмент в поиске и исследовании, проверке фактов и корректуре.