Дорогие коллеги!

На днях в блоге Теренса Тао вышла интереснейшая статья Томаса Хейлза Можно ли доверять Lean? О надёжности формальной математики в эпоху ИИ

Томас Хейлз — математик, который доказал гипотезу Кеплера о плотнейшей упаковке шаров, а потом вместе с коллегами потратил около двадцати человеко-лет на то, чтобы проверить это доказательство на компьютере. Мало кто имеет больше права говорить о надёжности формальных доказательств. Ниже — подробный пересказ его рассуждений с нашими пояснениями.

Ну а во вложении перевод оригинальной статьи на русский.

Что такое формальное доказательство

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

Программы для этого называют системами интерактивного доказательства (proof assistants). Их много: HOL Light, Isabelle, Rocq (бывший Coq), Mizar, Metamath. Среди математиков сейчас самая популярная — Lean, созданная Лео де Моурой в 2013 году. Вокруг неё выросла библиотека mathlib: почти 300 тысяч теорем, более 100 тысяч определений, 2,5 миллиона строк кода, сотни участников. Любой результат из неё можно использовать дальше — так же, как мы ссылаемся на известную теорему, а не передоказываем её.

Формализованы уже теорема о четырёх красках, теорема Фейта — Томпсона о группах нечётного порядка, гипотеза Кеплера, выворачивание сферы, задача об упаковке шаров в размерностях 8 и 24, Великая теорема Ферма.

2026 год: формализацией занялся ИИ

Главная перемена последних полутора лет — автоформализация. ИИ получает на вход статью в pdf или tex и сам выдаёт доказательство на Lean или в другой системе. Хейлз признаётся, что специалисты по формализации мечтали об этом десятилетиями, и вот мечта сбылась.

Хронология впечатляет. Осенью 2025 года компания Math Inc. с помощью ИИ (пока ещё с подсказками людей) формализовала теорему о распределении простых чисел. В январе 2026-го Йозеф Урбан за две недели получил 130 тысяч строк формальной топологии по учебнику Манкреса. В марте Math Inc. автоформализовала упаковку шаров в размерности 24 по доказательству Марины Вязовской и соавторов. В мае группа из Meta обработала значительную часть 26 учебников в проекте ATLAS.

Осенью — два громких события. Anthropic объявила об автоформализации Великой теоремы Ферма: 13 миллионов строк на Lean за 11 дней. OpenAI сопроводила свой результат о взрыве решений уравнений Навье — Стокса с внешней силой формальным доказательством на Lean. А Джаред Лихтман запустил проект MAP, цель которого — перевести в формальный код вообще всю известную математику.

На чём всё держится: ядро

Но если доказательства пишет ИИ, а проверяет программа, возникает естественный вопрос: а можно ли доверять самой программе?

В Lean всё устроено так. Пользователь (или ИИ) пишет доказательство на высокоуровневом языке. Система переводит его в низкоуровневую форму — этот этап называется элаборацией. Затем результат проверяет ядро — относительно небольшая программа на C++ (несколько тысяч строк), которая и выносит окончательный вердикт. Всё остальное может ошибаться сколько угодно: если ядро работает правильно, ложное доказательство не пройдёт.

Отсюда первое правило Хейлза: не верить доказательству на Lean, пока его не проверило ядро. И второе: даже проверенное доказательство нужно показать человеку, чтобы тот убедился, что доказано именно то, что нужно. Правильно ли определены вещественные числа, производные, мера? Совпадает ли формулировка теоремы с той, что стоит в условии задачи тысячелетия? Это гораздо проще, чем проверять само доказательство, но пропускать этот шаг нельзя.

Теория типов вместо теории множеств

Lean опирается не на привычную нам теорию множеств ZFC, а на теорию типов — точнее, на её вариант под названием «исчисление индуктивных конструкций».

Обе теории родились как ответ на парадокс Рассела. Цермело предложил аксиомы, которые просто не позволяют строить «опасные» множества. Рассел предложил иерархию типов, в которой парадоксальный объект нельзя даже записать — это синтаксическая ошибка.

Хейлз предлагает такую наглядную картинку. Множества можно рисовать кругами Эйлера — Венна, которые пересекаются. Типы — это кирпичи, уложенные вплотную, без пересечений: каждый объект принадлежит ровно одному типу. Число 2 как натуральное и число 2.0 как вещественное — разные объекты разных типов, между которыми есть явное отображение.

Для тех, кто беспокоится, что при переходе что-то потеряется: ещё в 1997 году Б. Вернер показал, что ZFC можно закодировать в теории типов, а теорию типов — обратно в ZFC с недостижимыми кардиналами.

«Лето ошибок корректности»

Самая страшная ошибка в системе доказательства — ошибка корректности: дефект ядра, позволяющий доказать «Ложь». А из лжи, как известно, следует что угодно.

Такие ошибки находили и раньше. Сам Хейлз в 2003 году нашёл ошибку корректности в HOL Light, ядро которой занимает всего несколько сотен строк и считалось эталоном надёжности, — и до сих пор вспоминает об этом с гордостью. В Lean 4 до и после выпуска в 2023 году тоже было найдено несколько таких ошибок.

Но летом 2026 года их посыпалось сразу много. Исследователи безопасности натравили на ядро Lean передовые ИИ-модели — и те нашли несколько дыр. Одна позволила «опровергнуть» гипотезу Коллатца. Другая дала короткое «доказательство» гипотезы Кеплера — так Хейлз о ней и узнал. Её обнаружил Рамана Кумар, ещё несколько ошибок — Дэн Селсам из OpenAI с помощью специализированного ИИ. Все ошибки быстро исправили, mathlib перепроверили.

Хейлз считает это скорее хорошей новостью: дыры нашли люди, заинтересованные в надёжности, а не злоумышленники. Но и повод для тревоги очевиден.

Три способа защиты

1) Много независимых ядер

Для Lean уже написано около 25 альтернативных ядер. Доказательство о Навье — Стокса подтвердили больше десятка из них. Но и это не панацея: ошибку Коллатца не поймало устаревшее ядро Nanoda — потому что у него нашлась своя, другая ошибка, которая «пропустила» то же ложное доказательство. Разные ядра могут унаследовать одинаковые дефекты, особенно если их авторы подглядывали в исходный код основного ядра. Поэтому Хейлз мечтает о реализации «в чистой комнате», написанной без оглядки на оригинал, а также о запуске ядер на разных языках, разном оборудовании и разных операционных системах.

Заодно он советует написать собственное ядро Lean как лучший способ досконально изучить систему — и сетует, что студенты на это предложение пока не откликаются.

2) Формальная верификация самого ядра

Здесь сразу встаёт вторая теорема Гёделя о неполноте: система не может доказать собственную непротиворечивость. Значит, речь может идти только об относительной непротиворечивости: «если непротиворечива такая-то теория множеств, то непротиворечив и Lean».

Для HOL Light подобную работу проделали давно: Джон Харрисон, а затем проект Candle на основе CakeML. А главная новость этой осени — ядро Con-Leche Йоахима Брайтнера. Оно написано на Lean, его непротиворечивость доказана на Lean относительно ZF с иерархией недостижимых кардиналов, а код и доказательства сгенерировал Claude. Con-Leche проверило всю mathlib, а его собственное доказательство перепроверено более чем десятком других ядер. Хейлз называет этот проект одной из важнейших вех в истории Lean.

3) Развитие теории

И вот здесь, по мнению Хейлза, дела обстоят хуже всего. Основной текст о теории типов Lean — магистерская диссертация Марио Карнейро 2019 года — содержит ошибку и к тому же описывает устаревшую версию Lean 3.

Многие базовые свойства до сих пор остаются гипотезами. Например, единственность типизации: если терм имеет тип A и тип B, то A и B должны совпадать с точностью до определительного равенства. Звучит как нечто само собой разумеющееся — но это не доказано. Не доказаны и инъективность ?-типов, и вариант свойства Чёрча — Россера.

Есть и доказанный отрицательный результат: Карнейро показал, что определительное равенство в Lean неразрешимо. На практике это значит, что алгоритм иногда не может распознать, что два терма на самом деле равны.

А полного опубликованного доказательства непротиворечивости теории типов Lean относительно теории множеств, по словам Хейлза, нет вовсе. Карнейро утверждает, что знает обходной путь, но так его и не записал. Con-Leche доказывает близкое, но не тождественное утверждение.

Позиция автора

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

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

Хейлз поддерживает призыв Карнейро: если вы занимаетесь теорией типов — Lean нужна ваша помощь.

Постскриптум: можно ли доверять доверию?

В конце Хейлз вспоминает классическую лекцию Кена Томпсона «Размышления о доверии к доверию». Томпсон показал, что вредоносный код можно спрятать в компиляторе так, что его не обнаружит никакая проверка исходников.

Хейлз переносит этот сюжет на нашу ситуацию. Летом 2026 года ядро Lean прочёсывал ИИ. Как убедиться, что он не оставил там «закладку» — ошибку настолько тонкую, что люди её не найдут? Что, если ею же воспользовались при верификации Con-Leche? И что, если однажды её используют, чтобы «доказать» корректность программ, защищающих критическую инфраструктуру?

Перекрёстная проверка множеством ядер сильно снижает такой риск, но Хейлз настаивает: работа над основаниями математики, переданная ИИ, опасна без тщательной проверки людьми. 

Оригинал (на английском): [https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/]

Телеграм: t.me/ainewsline

Источник: terrytao.wordpress.com

Комментарии: