9 июля 2026 года на arXiv вышла работа об эксперименте с Lean 4 — системой формальной верификации математических доказательств. Исследователь Джозеф Миллер формализовал доказательство благополучной постановки нелинейного уравнения Власова методом среднего поля Добрушина. Итог: 299 деклараций, чистая аксиоматика без единой заглушки, около недели на ключевые теоремы и около месяца на полную формализацию. Математик не написал ни одной строки доказательства. Писал агент.
Контекст
Lean 4 — формальная система, в которой математические утверждения записываются так, что компилятор проверяет их машинным образом. Если код компилируется без sorry (заглушек, которые можно подставить вместо незаконченного доказательства), результат считается верифицированным. Это другой уровень надёжности по сравнению с рецензированием коллег: компилятор не устаёт и не пропускает шаги. Формальная верификация существует десятилетиями, но до недавнего времени требовала от математика работы с деталями на уровне тактик доказательства — труд медленный и экспертный.
Уравнение Власова — нелинейное дифференциальное уравнение из математической физики, описывающее эволюцию распределения частиц. Формализация его через маршрут Добрушина — существование, единственность, оценка устойчивости, предел среднего поля — это не учебная задача. Тем не менее именно её Миллер выбрал полигоном для нового рабочего процесса. Попутно из сборки выпал самостоятельный математический слой: 49 из 299 деклараций (около шестой части работы) — инструментарий оптимального транспорта с метрикой Вассерштейна-1 и теоремой двойственности Канторовича-Рубинштейна. Этот слой компилируется независимо и готов к включению в библиотеку Mathlib.
В последние годы над связкой LLM и формальных доказательств работает несколько крупных команд. Работа Миллера отличается форматом: не автономный агент, а ИИ под управлением человека. Методологический фрейм — «игра формализации»: цель, правила победы, количественные наблюдения. Причём правила игры намеренно не называют конкретный ИИ-инструмент — методология рассчитана пережить любой конкретный запуск.
Аналитика
Самое ценное в этом эксперименте — не факт формализации конкретного уравнения. Ценна демонстрация паттерна: ИИ-агент работает надёжно, когда цель чётко формализована, а человек удерживает архитектурный контроль. Математик в проекте занимался тем, чем занимается хороший технический руководитель: скоупил определения, направлял декомпозицию, закрывал пробелы в библиотеке. Агент исполнял. Ни один из уровней не подменял другой.
«Формализация удостоверяет доказательство каждого утверждения в том виде, в каком оно записано; является ли записанное утверждение именно той теоремой, которую имел в виду автор, — остаётся суждением математика.»
Это не оговорка — это архитектурный принцип. ИИ гарантирует корректность внутри заданных рамок. Правильность самих рамок остаётся за человеком. Именно так должна выглядеть автоматизация сложного интеллектуального труда: не замена суждения, а усиление исполнения. Для бизнеса это означает, что критерий выбора задачи для ИИ-агента — не «достаточно ли она проста?», а «достаточно ли чётко сформулирована победа?»
Побочный артефакт — самостоятельный математический слой — говорит об ещё одной вещи. Качественная работа агента под руководством человека производит повторно используемые компоненты. Это не случайность, а следствие структурированной декомпозиции. В программировании это называется чистой архитектурой. Здесь то же самое — только в формальной математике.
Кейсы применения в бизнесе
B2B SaaS стартап. Если у вас есть критический алгоритм — расчёт тарифов, кредитный скоринг, распределение ресурсов — его можно формально верифицировать. Не тестами (тесты проверяют конечный набор сценариев), а доказательством. Рабочий процесс: старший инженер описывает инварианты на естественном языке, ИИ пишет Lean-код, компилятор верифицирует. Ценность для клиентов и регуляторов — не просто документация, а машинно-подтверждённая корректность логики.
Корпорация с legacy. Формальная верификация всего legacy-кода — нереалистична. Формальная верификация одного критического модуля — вполне. Выбери компонент с наибольшим риском: платёжная логика, механизм авторизации, расчёт скидок. Команда описывает желаемые инварианты, ИИ-агент под руководством инженера переводит в Lean, получаете машинную гарантию. Это не полная замена тестов, но дополнительный уровень уверенности там, где ошибка дорого стоит.
SMB в КР и Центральной Азии. Для большинства небольших компаний полная формальная верификация — избыточна сегодня. Но паттерн «директор-исполнитель» применим шире: написание тестов, генерация документации, рефакторинг под надзором инженера. Принцип идентичный: инженер задаёт цель и критерий победы, агент исполняет, человек контролирует результат. Это снижает время на рутину без потери контроля качества.
Кейсы в личной жизни
Разработчик. Попробуй описать инвариант одной функции — входные условия, гарантируемый выход — и попросить Claude написать Lean 4 theorem statement. Не нужно знать Lean в совершенстве: нужно понимать, что именно ты хочешь доказать. Хороший старт — функции сортировки, парсинга или валидации, где корректность поддаётся точному определению.
Студент или исследователь. Если пишешь статью с математическим доказательством — попробуй формализовать хотя бы один ключевой шаг в Lean 4 с ИИ. Это не только проверка: ты куда глубже понимаешь структуру доказательства, когда тебе нужно объяснить её агенту достаточно точно для исполнения. Ошибки в рассуждении всплывают немедленно — компилятор не прощает туманных формулировок.
Фрилансер или технический писатель. Паттерн из этого эксперимента применим к любой задаче с чёткими критериями завершения. Если ты умеешь формулировать «что значит сделано хорошо» — ты уже можешь быть директором для ИИ-агента. Не метафора, а рабочий принцип, который здесь проверен на одном из самых строгих классов задач.
Как применить сегодня
- Установи Lean 4 и расширение для VS Code. Попроси Claude объяснить синтаксис на конкретном маленьком примере — это быстрее любого официального туториала.
- Выбери одно утверждение, которое ты понимаешь, и задай его форму агенту: «Напиши Lean 4 theorem statement для свойства X функции Y». Оцени, насколько агент понимает задачу и где буксует.
- При сложных задачах держи декомпозицию за собой: ты определяешь, что формализовать и в каком порядке. Агенту отдаёшь тактику исполнения, не структуру.
- Обсуди с командой, какие модули кода имеют достаточно чёткие инварианты для эксперимента. Это первые кандидаты на верификацию.
- Следи за Mathlib — главной библиотекой Lean 4. Объём верифицированной математики в ней растёт, и это ускоряет любую новую формализацию: часть работы уже сделана за тебя.