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

Стартап Resolution (раньше он назывался Sequent) опубликовал отчёт о том, как автоматизировал формализацию разрешения особенностей Хиронаки. Краткий разбор появился в рассылке Import AI 478 у Джека Кларка, и там же приведены цифры, которые обычно держат за закрытыми дверями: сколько токенов ушло, сколько стоил проект и сколько строк кода получилось на выходе.

Что такое автоформализация

Автоформализация это перевод математического утверждения и его доказательства на язык proof assistant, в данном случае Lean. Результат проверяется механически: если ядро Lean приняло файл, значит в доказательстве нет логических дыр, пропущенных случаев и неявных «очевидно». Человеческое доказательство таких гарантий не даёт никогда, потому что его читают другие люди, а не компилятор.

Разница принципиальная. Ошибка в статье 1964 года может десятилетиями жить в литературе, пока кто-то не упрётся в неё при построении теории. Ошибка в Lean-файле ловится в момент компиляции.

Почему Lean, а не бумага

Lean это не язык программирования в привычном смысле, а proof assistant на теории зависимых типов. Утверждение в нём записывается как тип, доказательство как терм этого типа, а проверка сводится к проверке типов. Ядро у Lean маленькое, и его специально держат маленьким, чтобы доверие к нему не размывалось десятками слоёв логики.

Есть практическая деталь, которую обычно упускают. Lean разрешает оставлять заглушки sorry: файл компилируется, но в доказательстве остаётся дыра. Значительная часть работы в таких проектах уходит на то, чтобы вычистить все sorry и не дать им тихо переехать в финальную сборку. Шестьсот тысяч строк из отчёта Resolution это не только доказательство одной теоремы, но и библиотека вспомогательных лемм, которую дальше можно переиспользовать в других формализациях.

Как выглядел конвейер

Работа шла не одним запросом к модели, а оркестром агентов. Исследователь сначала собрал вместе с агентами два плана: короткий, понятный человеку, и детальный на 112 страниц, разбитый на атомарные шаги и привязанный к существующей литературе. Дальше включался оркестратор, который поднимал агентов под конкретные задачи: одни делали математику на бумаге, другие писали код на Lean, третьи проверяли, что процесс не съехал с плана.

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

Это переворачивает привычную картину. Обычно дорогим считают именно исполнение, а планирование воспринимают как что-то, что делается по ходу. Здесь наоборот: 112 страниц плана оказались той инвестицией, которая позволила запустить сотни агентов и не утонуть в противоречиях.

Что именно формализовали

Теорема Хиронаки о разрешении особенностей появилась в 1964 году и описывает, как устроены особенности алгебраических многообразий, то есть точки, где объект перестаёт быть гладким. Доказательство известно своей длиной и техничностью, и до сих пор его полная машинная проверка считалась задачей на годы человеческого труда.

Для Resolution это не абстрактное упражнение. Компания занимается теорией сингулярного обучения (singular learning theory, SLT), а она описывает поведение нейросетей через геометрию ландшафта функции потерь вблизи особых точек. Термин ввёл Сумио Ватанабе, и ключевая идея в том, что сложность модели определяется не числом параметров, а алгебраической геометрией её функции потерь. Отсюда и интерес к разрешению особенностей: без формализованного аппарата рассуждения об этой геометрии остаются на уровне интуиции.

Resolution пишет, что уже использует построенную библиотеку, чтобы продвинуть части SLT. Формализация разрешения особенностей позволяет автоматизировать больше теории, например лучше понять сэмплирование, а это понимание даёт рычаг на то, как модели учатся. Собственный термин компании для этого рычага, patterning, звучит достаточно туманно, но направление понятное: не гадать, почему модель обобщает, а выводить это из проверяемых утверждений.

Экономика строки

Самая полезная часть отчёта это бюджет. Около 100 миллиардов входных токенов, из которых 90% пришлись на чтения из кеша. Около 300 миллионов выходных токенов. Итоговая оценка расходов, 135 тысяч долларов. На выходе примерно 600 тысяч строк Lean.

Если разделить одно на другое, строка проверяемого доказательства обходится примерно в 22 цента. Цифра кажется большой, пока не сравнишь её с альтернативой: человеко-год специалиста по формальной математике стоит дороже, а главное, такие специалисты в дефиците и их время уходит на другие проекты.

Соотношение токенов важнее самой суммы. Входных токенов в 333 раза больше, чем выходных, и девять из десяти входных читаются из кеша. Это значит, что реальный счёт определяется не генерацией, а тем, сколько контекста система перечитывает на каждом шаге. Кеширование префикса здесь не оптимизация второго порядка, а основной рычаг: при падении доли кеш-чтений с 90% до 50% тот же проект стоил бы кратно дороже при том же объёме полезной работы.

Для практики вывод простой. Если вы строите похожий конвейер, бюджет надо планировать не по числу запросов, а по структуре контекста и по тому, какая часть работы повторяется. Агент, который каждый раз заново читает всю документацию, съест больше, чем агент, который один раз строит план и дальше работает по нему.

Та же кривая в софте

Пока математики обсуждают доказательства, рядом разворачивается почти идентичная история с программами. В той же рассылке есть бенчмарк ProgramBench, который вышел в мае 2026 года и проверяет, умеет ли модель собрать работающую программу по скомпилированному бинарнику и документации. В наборе 200 задач: интерпретаторы вроде PHP, Lua и tinycc, базы данных вроде DuckDB и SQLite, утилиты сжатия и работы с медиа вроде FFmpeg, zstd и xz, инструменты разработчика вроде ripgrep, fzf и jq.

В момент выхода бенчмарка лучший результат был нулевым. Claude Opus 4.7 набрал 0% по метрике resolved, то есть не решил полностью ни одной задачи из двухсот, и 3% по метрике almost, где проходят больше 95% тестов. К октябрю Claude Opus 5.5 в режиме xhigh получил 18.5% resolved и 70.5% almost.

Прогресс с 0% до 18.5% за несколько месяцев это не плавная кривая улучшений, а смена режима. Семьдесят процентов задач, где модель проходит почти все тесты, означают, что она уверенно воспроизводит структуру сложной программы и ошибается на краевых случаях. До полноценной замены инженеров ещё далеко, но экономика переписывания legacy-кода уже меняется.

Связь с математикой здесь не метафорическая. И доказательство в Lean, и пересобранный SQLite это артефакты с автоматической проверкой. Именно поэтому по ним можно строить графики прогресса, тогда как по «стало лучше отвечать на вопросы» нельзя.

Кто ещё на этом поле

Resolution не одинока. DeepMind довела свою систему AlphaProof до серебряного уровня на международной олимпиаде по математике в 2024 году: вместе с AlphaGeometry 2 она взяла четыре задачи из шести. Теренс Тао запускал проект, где сотни участников параллельно проверяли в Lean гипотезы про алгебраические тождества. Появились бенчмарки вроде miniF2F и PutnamBench, которые измеряют не «понимание математики», а долю задач, доведённых до состояния, когда ядро говорит да.

Закономерность одна и та же. Там, где появляется автоматическая проверка, прогресс становится измеримым, а измеримый прогресс ускоряется. Именно это, а не отдельная теорема, и есть главный сдвиг.

Где узкое место

Соблазн прочитать отчёт Resolution как «ИИ решил математику» велик, но он неверен. Теорема была известна с 1964 года, работа заключалась в переводе, а не в открытии. Это важное различие, и Resolution его не скрывает: они говорят об индустриализации математики, а не о новом результате.

Дальше начинаются скучные, но реальные ограничения. Ядро Lean считается доверенным, и если в нём есть ошибка, она обесценивает всё, что на нём построено. Шестьсот тысяч строк надо поддерживать: обновления библиотек, изменения синтаксиса, переименования в mathlib ломают сборку так же, как в обычном коде. Проверка типов не проверяет полезность: можно идеально формализовать утверждение, которое никому не нужно.

Есть и риск, о котором говорят меньше. Формализация смещает усилия в сторону того, что поддаётся формализации, а большая часть живого математического мышления пока этому не поддаётся. Если награда за проверяемость станет слишком большой, исследователи могут начать выбирать задачи по критерию удобства для Lean, а не по научной ценности.

Что делать командам

Если вы работаете с агентами, а не с математикой, из этого отчёта выжимаются три практических урока.

Первый: инвестируйте в план, а не в промпты. Сто двенадцать страниц атомарных шагов звучат как избыточность, но именно они позволили исполнению идти почти без обвязки. Дешёвое исполнение вырастает из дорогого планирования.

Второй: считайте стоимость проверяемого артефакта, а не стоимость диалога. Токены сами по себе ничего не говорят. Полезная метрика это сколько стоит один принятый тестами результат, потому что она сразу показывает и цену генерации, и цену переделок.

Третий: проектируйте контекст под кеш. Девяносто процентов кеш-чтений в проекте Resolution это не случайность, а архитектурное решение. Агентские пайплайны, которые пересобирают контекст с нуля, платят за это трижды.

Часто задаваемые вопросы

ИИ доказал новую теорему?

Нет. Речь о формализации уже известного результата, теоремы Хиронаки 1964 года. Работа состояла в переводе существующего доказательства на язык Lean и его машинной проверке, а не в открытии нового математического факта.

Почему формализация стоила 135 тысяч долларов?

Основную часть счёта составили входные токены, около 100 миллиардов, из которых 90% читались из кеша. Выходных токенов было всего около 300 миллионов, но каждый шаг агентов требовал заново подавать большой контекст, и именно это определило итоговую сумму.

Заменит ли это математиков?

В обозримом будущем нет, но работа изменится. Рутинная часть, связанная с переводом известных результатов в проверяемый вид, уходит агентам. Людям остаётся выбирать задачи, ставить гипотезы и решать, что вообще стоит формализовать.

Итог

Автоформализация математики перестала быть исследовательской экзотикой и стала вопросом бюджета. Неделя, 135 тысяч долларов и 600 тысяч строк Lean выглядят как дорогая игрушка ровно до того момента, когда вы вспоминаете цену человеко-года в этой области и размер очереди неформализованных результатов.

Следующий шаг здесь не в том, чтобы восхищаться цифрами, а в том, чтобы понять свою нишу. Если в вашей работе есть артефакты с автоматической проверкой, тесты, типы, доказательства, спецификации, то к ним уже применима экономика Resolution. Начните с одного такого артефакта и посчитайте, во что обходится его полная проверка сегодня.