Верификация кода становится рабочим контуром ИИ-разработки В один день сошлись две новости: Mistral выпустила Leanstral, специализированную открытую модель для функционального языка программирования и системы автоматического доказательства теорем Lean 4, а Theorem показала lf-lean — практически промышленный конвейер, где ИИ не просто переводит код, а доказывает корректность результата. Leanstral — это не «ещё один помощник программиста». Модель заточена под Lean 4, то есть под среду формальной проверки и доказательства свойств программ. Ключевой момент здесь не генерация кода как таковая, а генерация кода, который можно формально проверить. Mistral прямо бьёт в узкое место ИИ-разработки: код модели пишут быстро, а человеческая проверка становится бутылочным горлышком. В этой логике следующий шаг очевиден: не просить человека разбирать машинный код постфактум, а заставить машину сразу выдавать артефакт, проверяемый доказателем. И тут очень кстати выходит lf-lean. Компания Theorem показала, как это выглядит в масштабе. Их система rocq-dove автоматически строит спецификацию корректности для целого класса задач — в данном случае для перевода из языка функционального программирования Rocq в Lean — и затем проверяет, что перевод и доказательство действительно совпадают по смыслу. Результат впечатляющий: из 1276 утверждений из учебника Logical Foundations, около 97% ИИ перевёл и верифицировал автономно. Остаток уперся всего в 6 «экстремально сложных» мест, где понадобилось примерно 15 часов ручной работы. Авторы оценивают, что полностью вручную это заняло бы около трех лет. Связка этих двух новостей очень важна. Leanstral даёт специализированный инструмент для работы в среде формальных доказательств. lf-lean показывает, что такой инструмент уже можно встраивать в масштабируемый процесс разработки, а не только в исследовательские демонстрации. Практически это важно ещё и потому, что подход не привязан к зарубежному софту. Leanstral доступна как открытая модель на Hugging Face, а стек вокруг Lean, Rocq и lf-lean поднимается локально из репозиториев, а значит его можно разворачивать в российских облаках или на изолированных серверах организации. Источник: https://eyes.etecs.ru/r/1714ce #вайбкодинг