В ядре Lean нашли баг, нарушающий soundness: #14576. Рамана Кумар с помощью ИИ опубликовал «опровержение» гипотезы Коллатца без sorry — оно эксплуатировало ошибку во вложенных индуктивных типах. Киран Гопинатан свёл его к доказательству False и открыл issue #14576. Патч #14577 вышел через час, после ревью Иоахима Брайтнера его влили.
Суть бага: когда ядро устраняет вложенное вхождение под индуктивным типом T с параметрами Ds, фантомные параметры исчезают из вспомогательного типа и не проверяются. Через это можно протащить плохо типизированный аргумент и заставить ядро принять proof of False. Достижимо только через метапрограммирование — отправкой объявления прямо в ядро. Фронтенд такие аргументы отсекает. Это баг реализации, а не дыра в мета-теории.
nanoda не поймал баг, потому что в нём был свой. Это независимое ядро Lean на Rust от Криса Бейли. Оно проверяло нужное место, но не проверяло имя типа в projection node. Официальное ядро — наоборот. Баг nanoda исправили за неделю до бага Lean. Доказательство устроили так, что выражение, которое не проверяет ядро, старая nanoda принимала. Рамана считает совпадение случайным, но не исключает, что модель видела отчёт. Иоахим предположил, что сильные модели теперь умеют находить такие баги. Вывод: независимая проверка работает, но нужны свежие версии обоих инструментов.
lean4lean тоже затронут: его обработка индуктивных — порт официального ядра. Это формализация теории типов Lean с доказательством корректности от Марио Карнейро. Индуктивные типы пока не покрыты, и реализация содержит тот же баг.
Предложение ограничить метапрограммирование ошибочно. Элаборатор недоверен по дизайну, soundness не может зависеть от недоверенного компонента. Атакующий может написать .olean-файл или изменить память, минуя элаборатор. Ядро должно само отклонять плохие объявления.
Lean FRO добавил тесты в Kernel Arena, PR #14582 ужесточает проверку параметров. Дэниел Селсам из OpenAI помог с ИИ для кибербезопасности: нашлись другие ошибки в ядре, все, как и первый, достижимы только через метапрограммирование, все исправлены (PR #14607–#14616) и все пойманы nanoda. Укреплены инварианты ядра (#14621, #14631, #14632). comparator.live теперь использует nanoda по умолчанию. Lean FRO также поддерживает экспертов, которые ищут баги и разрабатывают новые или верифицированные ядра.