Lean устранила критическую уязвимость ядра, вскрытую ИИ-«опровержением» гипотезы Коллатца

Lean FRO, организация, которая разрабатывает язык и доказчик теорем Lean, опубликовала подробный разбор критической уязвимости ядра, ошибки корректности (soundness) под номером #14576. Баг обнаружили и устранили за неделю, начавшуюся 27 июля 2026 года. Толчком послужило то, что 25 июля Рамана Кумар выложил репозиторий с «опровержением» гипотезы Коллатца без пропусков (sorry-free), составленным с помощью ИИ. Доказательство оказалось не настоящим: оно эксплуатировало дыру в обработке ядром вложенных индуктивных типов. 28 июля Киран Гопинатан свёл этот эксплойт к минимальному доказательству False и завёл issue #14576; фикс (PR #14577) выложили через час после сообщения, Йоахим Брайтнер проверил его и предложил улучшения, после чего изменения слили в основную ветку, и вышли новые патч-релизы.

Механизм ошибки: когда ядро обрабатывает вложенное вхождение индуктивного типа T с параметрами Ds, а эти параметры «фантомные», то есть не упоминаются в полях конструкторов, они пропадают из автоматически порождаемого вспомогательного типа и не попадают под проверку типов. На это место можно подставить некорректно типизированный аргумент и заставить ядро принять доказательство False. Добраться до уязвимого места можно только через метапрограммирование, отправив объявление индуктивного типа напрямую в ядро в обход штатной проверки аргументов на фронтенде (elaborator, модуль вывода термов). Это ошибка конкретной реализации, а не дыра в метатеории Lean.

Исходный репозиторий с «опровержением» проходил проверку и независимым checker'ом nanoda (реализация ядра Lean на Rust, автор, Крис Бейли), но лишь по случайному совпадению: у nanoda был отдельный, не связанный с первым, баг, она проверяла как раз то место, которое пропустило официальное ядро, но не проверяла имя типа в узле-проекции. Эту ошибку нашёл Джереми Чен, и её исправили за неделю до того, как сообщили об ошибке ядра Lean. Доказательство было построено так, что выражение, которое официальное ядро никогда не проверяет, это ровно то выражение, которое старая версия nanoda пропускала. Рамана Кумар считает совпадение по времени случайным, но не исключает, что модель могла видеть отчёт об ошибке nanoda; Йоахим Брайтнер предположил, что совпадение объясняется просто доступностью достаточно сильных моделей, способных находить такие баги. Практический вывод: проверка независимым ядром по-прежнему работает как защита, поскольку для обхода нужны две разные ошибки в двух разных реализациях, но только если обе реализации обновлены до актуальных версий. Формализация lean4lean Марио Карнейро (доказательство того, что ядро Lean реализует его типовую теорию) затронута тем же багом, поскольку обработка индуктивных типов там, порт эталонной реализации; сама эта ошибка была бы найдена при завершении проверки консистентности для индуктивных типов, которая пока не закончена.

В обсуждении звучало предложение убрать или ограничить метапрограммирование, чтобы такую атаку нельзя было выразить. Автор поста называет это ошибочным подходом: elaborator по конструкции недоверенный компонент, и корректность системы не может зависеть от того, что недоверенный компонент сам откажется строить плохой терм. Атакующий, который хочет подсунуть вредоносное доказательство, может и напрямую написать файлы .olean или изменить память в обход elaborator'а целиком, поэтому именно ядро обязано само отвергать некорректно типизированные объявления в своём собственном процессе; это разделение ответственности, одно из главных преимуществ архитектуры Lean на термах доказательств.

После инцидента Lean FRO предприняла несколько шагов. В Kernel Arena (набор регрессионных тестов для ядра) добавили тесты на этот эксплойт и на смежный случай с неоднородными параметрами, о котором сообщил Артур Аджедж. Отдельный follow-up PR (#14582) заставляет ядро проверять, что параметры вложенного вхождения действительно ведут себя как параметры, а не просто повторно проверять их типы. Дэниел Селсам из OpenAI помог Lean FRO прогнать по ядру специализированный на кибербезопасности ИИ, который нашёл ещё шесть отдельных программных ошибок (PR #14607, #14608, #14609, #14613, #14615, #14616), все они, как и первая, доступны только через метапрограммирование, все исправлены, и все были бы пойманы nanoda. Ещё тремя PR (#14621, #14631, #14632) усилили внутренние инварианты ядра. Сайт comparator.live теперь по умолчанию запускает nanoda, а сам nanoda и связанные с ним lean-eval и comparator отслеживаются ежедневно, чтобы оставаться актуальными после апстрим-исправлений. Lean FRO также ищет и поддерживает специалистов, способных находить новые баги, разрабатывать новые ядра и работать над теорией или верифицированными реализациями.

Ключевые факты

Баг #14576 в ядре Lean позволял доказать False: фантомные параметры вложенного индуктивного типа выпадали из проверки типов, и через метапрограммирование туда можно было подставить некорректный терм.
Обнаружился он благодаря тому, что 25 июля Рамана Кумар выложил ИИ-сгенерированное «опровержение» гипотезы Коллатца без sorry, на деле оно эксплуатировало этот баг; 28 июля Киран Гопинатан свёл его к минимальному доказательству False и открыл issue.
Фикс (PR #14577) выложили через час после открытия issue; независимый checker nanoda пропустил ту же атаку из-за отдельной, не связанной ошибки в проверке имени типа в узле-проекции, её нашёл Джереми Чен и исправил неделей раньше.
После разбора Дэниел Селсам из OpenAI прогнал по ядру специализированный ИИ по кибербезопасности, который нашёл ещё шесть программных ошибок в ядре, все исправлены.
Lean FRO добавила регрессионные тесты, ужесточила инварианты тремя отдельными PR и теперь ежедневно прогоняет nanoda на comparator.live, чтобы обе реализации ядра оставались синхронизированы.

Почему это важно

Ядро доказчика теорем, корень доверия ко всей формальной верификации: если оно может принять доказательство False, под сомнением оказываются все теоремы, проверенные уязвимой версией, включая крупные библиотеки формализованной математики. История показывает и обратную сторону ИИ: та же генеративная модель, которая помогла построить «опровержение» известной гипотезы, на практике нащупала реальную дыру в критической инфраструктуре, то есть ИИ-инструменты уже способны случайно (а потенциально и целенаправленно) находить уязвимости корректности в проверяющем ПО. Это первый публичный кейс такого рода для Lean, разобранный подробно, с точными номерами issue и PR, а не общими словами.

Кому это важно

Прежде всего, сообществу Lean и mathlib: математикам, формализующим доказательства, и инженерам, использующим Lean для верификации кода и протоколов, где корректность ядра, единственная гарантия. Важно и для разработчиков независимых checker'ов вроде nanoda, и для команд, строящих верифицированные реализации (lean4lean Марио Карнейро). Отдельно это касается специалистов по безопасности ИИ-систем: случай показывает, что ИИ-ассистированный поиск доказательств уже натыкается на реальные уязвимости в проверяющем ПО, а привлечение специализированного ИИ (Дэниел Селсам, OpenAI) к аудиту кода оказалось рабочим приёмом, так нашли ещё шесть ошибок.

Как это применить

Пользователям Lean и nanoda стоит обновиться до пропатченных версий (issue #14576, PR #14577 и #14582 для ядра; актуальная версия nanoda после исправления, найденного Джереми Чен) и обновлять обе реализации одновременно, защита независимым ядром работает, только если версии обеих актуальны. Идею «просто отключить метапрограммирование», чтобы закрыть класс уязвимостей, стоит признать неверной: любое архитектурное решение должно исходить из того, что фронтенд (elaborator) в принципе недоверен, а именно ядро обязано само отвергать некорректные термы. Командам, проверяющим критичный код, имеет смысл присмотреться к практике Lean FRO, прогонять специализированный по кибербезопасности ИИ поверх обычного ревью: в этом случае он нашёл шесть дополнительных ошибок, которые иначе остались бы незамеченными.

Можно ли доверять

Это первоисточник, официальный пост-мортем от Lean FRO с точными номерами issue и PR, датами и раскрытием технического механизма, а не пресс-релиз. Текст рецензировали названные по именам инженеры (Йоахим Брайтнер и Себастьян Ульрих), что повышает достоверность деталей. При этом текст не даёт окончательного ответа, видела ли ИИ-модель более ранний отчёт об ошибке в nanoda, это открытый вопрос, честно обозначенный как неопределённость самим Раманой Кумаром.

Риски и подводные камни

Независимый checker, не панацея: nanoda проверяла как раз то место, которое не проверяло исходное ядро, но не другое, то есть у проверяющих систем тоже есть слепые пятна, и их нельзя считать гарантией без учёта конкретной версии. Пока метапрограммирование остаётся частью Lean, любой ещё не найденный баг в обработке присылаемых напрямую объявлений, системная точка отказа, единственная линия защиты от которой, код самого ядра. Пользователи на устаревших версиях Lean или nanoda остаются уязвимы даже после выхода патчей. Наконец, тот же инцидент подсвечивает обратный риск: ИИ, способный случайно найти такую дыру при попытке «доказать» математическую гипотезу, в принципе способен и целенаправленно искать подобные уязвимости в другом проверяющем ПО.

«Это ошибка конкретной реализации, а не дыра в метатеории Lean.»

— автор поста в блоге Lean FRO