Новая парадигма: ИИ-формализация как стратегическая игра
В статье, опубликованной в arXiv (cs.AI), описывается новый подход к верификации сложных математических доказательств. Автор предлагает рассматривать процесс формализации в системе Lean 4 не как рутинную работу, а как «стратегическую игру». В этой модели роль человека сводится к высокому уровню управления: постановке целей, декомпозиции задач и устранению пробелов в библиотеках. ИИ-агент берет на себя техническую реализацию — перевод LaTeX-документов в код Lean.
Ключевое условие победы в этой «игре» — компиляция разработки без использования конструкции sorry (заглушки) и гарантия того, что целевые теоремы опираются исключительно на аксиомы Lean. Второе критерием успеха является «переиспользование»: создание самодостаточного слоя общей математики, который может быть интегрирован в более широкие библиотеки.
Кейс-стади: Уравнение Власова и метрики оптимального транспорта
В качестве тестового полигона была выбрана задача о корректности нелинейного уравнения Власова (существование, единственность, оценка устойчивости и предел среднего поля) по методу Добушина. Процесс позволил выделить отдельный блок машинного транспорта, включающий свойства метрики Wasserstein-1 и теорему о двойственности Канторович-Рубинштейна.
Результаты формализации демонстрируют высокую степень модульности. Выделенный блок оптимального транспорта компилируется против Mathlib самостоятельно и составляет около шестой части от всей разработки.
| Метрика | Значение / Описание |
|---|---|
| Всего деклараций | 299 |
| Деклараций в блоке оптимального транспорта | 49 (≈16% от общего объема) |
| Размер интерфейса | 22 декларации (без обратных зависимостей) |
| Время на headline-теоремы | ~1 неделя |
| Время на полную разработку | ~1 месяц |
Роль человека и машины
Автор подчеркивает разделение ответственности. ИИ-агент выполняет кодирование и проверку синтаксиса, но математическая корректность формулировок остается на совести исследователя. Человек определяет, является ли записанное утверждение тем самым теоремой, который он хотел доказать. Такой подход позволяет масштабировать формализацию, снижая порог входа для сложных разделов математической физики и анализа уравнений в частных производных (PDE).
Значение для сообщества
Работа Joseph K. Miller показывает, что гибридные системы «человек-ИИ» способны справляться с задачами, требующими глубокого понимания структуры математических доказательств. Методологический фреймворк, описанный в статье, не привязан к конкретным ИИ-моделям, что делает его универсальным инструментом для будущих исследований в области компьютерной проверки доказательств.
Источник: arXiv cs.AI ↗