Леонардо де Моура — фигура фундаментальная для мира формальных методов. Создатель языка программирования Lean и соавтор знаменитого решателя Z3, он посвятил десятилетия тому, чтобы сделать математические доказательства и проверку ПО механически неоспоримыми. В большой беседе с ведущим канала Machine Learning Street Talk Тимом Скарфом он рассказал, как его проект из «лабораторного» инструмента превратился в глобальный феномен, как ИИ пытается взламывать математическую истину и почему будущее программирования немыслимо без формальных сертификатов.
🏛️ Собор против Базара: управление ядром Lean 0:59
Де Моура объясняет, что разработка Lean следует модели «Собора», где центральная группа жестко контролирует то, что попадает в ядро системы . Это осознанный выбор: в отличие от обычных библиотек, где отсутствие функции — лишь временное неудобство, «дырявая» система формальной верификации бесполезна .
Основные тезисы о структуре проекта:
- Lean FRO: Некоммерческая организация, в которой сейчас работают 20 человек, владеющих разными частями системы .
- Разделение ответственности: В то время как ядро (core) стабильно и защищено, сообщество развивает колоссальную библиотеку Mathlib и собственные расширения без прямого участия де Моуры .
- Расширяемость: Lean 4 был переписан так, чтобы пользователи могли создавать доменные языки (DSL) поверх него, не меняя основной код. В качестве примера де Моура приводит проект профессора Ильи Сергея из Сингапура по верификации императивного ПО, который поразил автора своей проработанностью .
🛡️ Инцидент с гипотезой Коллатца: когда ИИ ищет лазейки 11:12
Одним из самых резонансных событий «этой недели» (на момент записи) стала попытка публикации ложного опровержения гипотезы Коллатца . Некто представил доказательство на Lean, которое было принято официальным ядром системы и внешним чекером Nanoda.
Де Моура и его коллега Йоахим Брайтнер провели расследование и пришли к следующим выводам:
- Эксплойт двух багов: Доказательство содержало странные, на первый взгляд ненужные термы для создания хеш-коллизий . Оказалось, что оно одновременно эксплуатировало один баг в официальном ядре Lean и совершенно другой баг в Rust-реализации Nanoda .
- След ИИ: Де Моура твердо убежден, что этот эксплойт был создан ИИ. У человека не хватило бы терпения вручную подбирать параметры для таких низкоуровневых атак, тогда как модели могут генерировать тысячи вариантов, пока не увидят «зеленую галочку» подтверждения .
- Меры защиты: В Lean FRO теперь обсуждают введение баунти-программ за создание «непробиваемых» ядер и ускорение работы над проектом Lean4Lean Марио Карнейро, где корректность самого ядра доказывается математически .
🤖 Революция в кодинге: случай с zlib 21:59
Важной вехой стал эксперимент Кима Моррисона, который с помощью агента Claude переписал библиотеку сжатия zlib с языка C на Lean и формально доказал её корректность .
Результаты эксперимента оказались шокирующими для де Моуры:
- Корректность: ИИ доказал, что при любом уровне сжатия и любых входных данных декомпрессия возвращает оригинал .
- Производительность: После просьбы об оптимизации ИИ выдал код для работы с массивами, который обошел по скорости реализацию на Rust .
- Смена парадигмы: Де Моура признает, что еще год назад считал такие задачи недоступными для ИИ . Теперь он видит будущее, где программист пишет лишь высокоуровневую спецификацию («что я хочу вычислить»), а ИИ превращает её в сверхэффективный ассемблерный код, сопровождая это доказательством эквивалентности .
📚 Математика как бесконечная стройка 37:25
Библиотека Mathlib для Lean 4 уже содержит более 2,4 миллиона строк кода, значительно превзойдя версию для Lean 3 . Кевин Баззард, известный популяризатор Lean, утверждает, что формализованная математика всегда будет составлять «0%» от всей существующей, так как дисциплина растет быстрее, чем её успевают записывать в коде .
Де Моура выделяет два аспекта этого процесса:
- Дистилляция: Базовые понятия (кольца, группы) уже «кристаллизованы» и абстрагированы максимально эффективно .
- Frontiers: Проект Formal Frontiers ставит целью создать такую базу, чтобы любой современный исследователь мог формализовать свою новую статью, не отвлекаясь на описание основ, подобно тому как программист использует готовые «крейты» (библиотеки) в Rust .
🧠 Искусственный интеллект: компетентность без понимания 53:03
Обсуждая возможности LLM, де Моура соглашается с тезисом о «компетентности без понимания» . Модели отлично решают задачи типа «nut-sniping» (комбинирование известных трюков из литературы для закрытия пробела в доказательстве), но пасуют перед созданием принципиально новых теорий .
Ключевые мысли о роли человека:
- Целеполагание: Люди остаются авторами, потому что они выбирают, какие задачи достойны решения, и задают спецификации .
- Эстетика: Важные доказательства люди будут продолжать писать вручную, чтобы они были «красивыми» и пригодными для обучения других людей, а не просто представляли собой массив машинных инструкций .
- Сертификаты: Даже если ИИ станет ошибаться в 0.0001% случаев, нам всё равно нужны формальные сертификаты. Де Моура приводит в пример доказательство OpenAI для одной из гипотез, которое занимает 1,2 миллиона строк Lean — ни один человек не в силах проверить его глазами .
🚀 Будущее и советы новичкам 1:06:38
Леонардо де Моура смотрит в будущее с оптимизмом, утверждая, что если он уйдет из проекта сегодня, Lean продолжит жить благодаря FRO и сообществу .
Для тех, кто хочет начать изучение Lean, он дает неожиданный совет:
- Начните с программирования: Не пытайтесь сразу доказывать теоремы. Используйте Lean как обычный функциональный язык, привыкните к синтаксису .
- Используйте ИИ как тьютора: Современные модели (Claude, GPT) отлично знают документацию Lean. Им можно сказать: «Я разработчик на C#, объясни мне этот концепт на моих примерах», и они откалибруют объяснение .
