Lean v4.35.0 получил команду lake check и четыре дополнительных ядра проверки

Авторы Lean сообщают, что помощник доказательств Lean теперь поставляется с дополнительными ядрами проверки. Поводом названы две недавние публикации о разборе уязвимостей (от 1 и 24 августа): по словам авторов, ИИ-агенты очень эффективно находят уязвимости в программах, в том числе в ядре Lean (программе, которая проверяет доказательства). Команда укрепляет официальное ядро, добавляет новые и делает инструменты, облегчающие перепроверку проектов внешними ядрами.

В Lean v4.35.0 появилась команда lake check. Она экспортирует разработку и перепроверяет её через leanchecker, официальное ядро Lean без окружающего «багажа». Весь процесс идёт в песочнице; отключить её можно флагом lake check --inadvisably-no-sandbox. Вместе с Lean теперь поставляются четыре дополнительных ядра: nanoda, lean4lean, con-leche и con-ron. Перепроверить проект всеми ими можно командой lake check --paranoid; в этом режиме также запускается вариант официального ядра, собранный с усиленным распределителем памяти, который превращает порчу памяти в контролируемое аварийное завершение вместо молча неверного ответа.

Con-leche, по словам авторов, первое ядро для Lean, написанное на Lean и с доказанной непротиворечивостью. Его реализовал и доказал Claude (Fable и Opus) под плотным надзором Joachim Breitner из Lean FRO. «Непротиворечивость» здесь значит, что у каждого окружения, которое принимает con-leche, есть модель в теории множеств; доказательство следует модели теории типов Lean, предложенной Mario Carneiro. Само доказательство проверено официальным ядром Lean и опирается на допущение о непротиворечивости использованной теории множеств. Такой подход, как пишут авторы, устраняет целый класс ошибок, программистские ошибки в реализации ядра, без потери скорости: на полном экспорте Mathlib con-leche выполняет 0,69 от числа инструкций официального ядра и проверяет всю библиотеку примерно за 100 секунд на восьми потоках.

Со стопроцентной защитой это, однако, не сравнить: в компиляторе и среде выполнения, которыми собирают con-leche, могут быть ошибки. Чтобы снизить этот риск, Breitner с помощью ИИ перевёл con-leche на Rust и затем инструментом Aeneas (он проверяет код на Rust средствами Lean) доказал, что версия на Rust уточняет алгоритм проверки con-leche. Это ядро называется con-ron. Логика авторов: раз у con-leche есть формальное доказательство непротиворечивости, оставшиеся ошибки корректности, скорее всего, сидят в компиляторе или среде выполнения Lean (включая библиотеку длинных чисел), а совпадение такой же ошибки в компиляторе или среде Rust очень маловероятно. Поэтому проверка и con-leche, и con-ron даёт высокий уровень защиты от этого класса ошибок.

Дальше планы: авторы ожидают завершить в ближайшие несколько месяцев верификацию lean4lean, тогда в поставке будет три верифицированных ядра. Эта верификация важна ещё и потому, что реализация lean4lean очень близка к официальной реализации ядра на C++. Arthur Adjedj занимается планом обновления ядра (задача #14977) и уже отправил несколько запросов на слияние; Breitner их проверяет, следит, чтобы con-leche реализовывало те же изменения, и правит доказательство, чтобы не появилось новых «дыр». Adjedj также работает над ещё более простыми ядрами для Lean.

Список нерешённого: более удобная lake check, возможность подключать к ней своё ядро (в Lean Kernel Arena уже есть несколько новых эффективных ядер), верификация частей компилятора. Отдельная проблема, масштаб: Anthropic FLT насчитывает свыше 13 млн строк кода, Mathlib, 2,5 млн, Tau Ceti, уже больше 3 млн и быстро растёт, репозиторий общей теоремы Куртада, Кумара, выше 50 млн, а сообщество пишет предложения библиотек на 1 млрд строк и более. Нынешний подход к внешним ядрам на таких объёмах не масштабируется; нужны двоичные форматы экспорта и инкрементальная проверка внешними ядрами. Пока же авторы советуют запустить lake check --paranoid на своём проекте, а если ядра разойдутся во мнении о доказательстве, написать на contact@lean-fro.org.

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

Lean v4.35.0 включает команду lake check: она экспортирует проект и перепроверяет его через leanchecker (официальное ядро) в песочнице; режим lake check --paranoid запускает ещё четыре ядра, nanoda, lean4lean, con-leche, con-ron, и официальное ядро с усиленным распределителем памяти.
Con-leche, по словам авторов, первое ядро для Lean, написанное на Lean и с доказанной непротиворечивостью; его реализовал и доказал Claude (Fable и Opus) под плотным надзором Joachim Breitner из Lean FRO.
На полном экспорте Mathlib con-leche выполняет 0,69 от числа инструкций официального ядра и проверяет библиотеку примерно за 100 секунд на восьми потоках.
Con-ron, перевод con-leche на Rust, для которого с помощью Aeneas доказано уточнение алгоритма con-leche; вместе два ядра защищают от ошибок в компиляторе и среде выполнения.
Нерешённая проблема, масштаб: проекты вроде FLT от Anthropic (свыше 13 млн строк) не проверяются нынешним подходом к внешним ядрам, нужны двоичные форматы экспорта и инкрементальная проверка.

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

Ядро, это программа, которая решает, считать ли доказательство верным; на нём держится доверие ко всей формализованной математике и проверенному коду в Lean. Авторы пишут, что ИИ-агенты очень эффективно находят уязвимости в ПО, в том числе в ядре Lean, и отвечают на это несколькими независимыми ядрами. Ключевая новизна, con-leche: ядро, чья непротиворечивость доказана формально, причём работу выполнила нейросеть под надзором человека, а итог проверил официальный Lean.

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

Прежде всего разработчикам и пользователям Lean и Mathlib, кто хочет перепроверить свои доказательства независимыми ядрами. Также тем, кто занимается формальной верификацией и интересуется тем, как ИИ применяют в доказательствах и проверке критичного кода, и авторам крупных формализованных библиотек, для которых проблема масштаба уже актуальна.

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

Обновитесь до Lean v4.35.0 и выполните в проекте lake check, он перепроверит разработку официальным ядром в песочнице. Для максимальной проверки запустите lake check --paranoid: он задействует nanoda, lean4lean, con-leche, con-ron и вариант официального ядра с усиленным распределителем памяти. Песочницу можно отключить флагом --inadvisably-no-sandbox, но название флага само говорит, что делать этого не стоит. Если ядра по-разному оценили ваше доказательство, авторы просят написать на contact@lean-fro.org.

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

Это запись самих разработчиков Lean, то есть первоисточник, но оценки в ней авторские: «первое ядро, написанное на Lean и с доказанной непротиворечивостью», «высокий уровень защиты». Доказательство непротиворечивости проверено официальным ядром Lean и опирается на допущение о непротиворечивости теории множеств, на которой построена модель. Цифры производительности (0,69 от инструкций официального ядра, около 100 секунд на восьми потоках) даны только для con-leche; авторы отсылают к файлу PERF.md. Верификация lean4lean пока лишь ожидается.

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

Сами авторы признают: con-leche не является абсолютно надёжным, так как в компиляторе и среде выполнения, которыми его собирают, возможны ошибки (включая библиотеку длинных чисел). Con-ron снижает этот риск, но опирается на предположение, что одинаковая ошибка в Rust крайне маловероятна. Для очень больших проектов (десятки и сотни миллионов строк) нынешний подход к внешним ядрам не масштабируется; пока нет и удобной подстановки собственного ядра в lake check, а работа над компилятором и двоичными форматами только планируется.