Axiom Math проверила 16 млн строк Lean-кода агентами и закрыла дыру в формальной математике

Когда ИИ каждую неделю «решает» новую математическую задачу, возникает резонный вопрос: кто всё это проверяет? Только за прошлый месяц OpenAI выпустила 719 рукописей с заявленными решениями сложных задач. Читать их все вручную невозможно, а ошибки проскакивают даже при машинных проверках. Стартап Axiom Math, оценённый в $1,6 млрд, предлагает другой путь: не замедляться, а встать на проверенный фундамент.

Что именно сделали

В среду компания объявила, что формально верифицировала Stacks Project — один из крупнейших в истории сводов человеческой математики. Его начал в 2005 году Йохан де Йонг из Колумбийского университета как открытый справочник. Сегодня там около 7654 страниц: от университетской алгебры до передовых идей алгебраической геометрии и теории чисел.

Агенты Axiom переписали всё это в виде около 16 млн строк кода на языке Lean. Затем программа, называемая proof assistant, проверила код строка за строкой. Если проверка прошла, доказательство логически корректно, и верить автору на слово не нужно.

Почему это сложнее, чем кажется

Проверить каждую теорему по отдельности — лишь полдела. Результаты в Stacks связаны друг с другом как семейное дерево: каждый опирается на предыдущие. Если где-то определение «поплыло», рушится всё, что стоит выше. Поэтому команде нужно было сохранить все связи на протяжении 16 млн строк. Сама CEO Карина Хонг признаёт, что сначала не была уверена в успехе: большое и хрупкое плохо сочетаются.

Архитектура была такой: сверху мягкая иерархия, но без жёсткого распределения задач. Агенты сами находили, чем заняться, и работали параллельно. Axiom также обучила собственные модели для математики, чего, по словам Хонг, большинство конкурентов в верификации не делает. Сначала штатный эксперт по Lean прививал агентам «вкус» — понимание, как должен выглядеть хороший код. Со временем, говорит Хонг, они стали справляться сами.

Зачем это разработчикам

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

Ставка Axiom: математика — полигон, где этот навык отрабатывается, а затем переносится на софт. Агенты могут читать готовую Lean-библиотеку и строить на ней новое, не начиная с нуля. Терренс Тао формулирует общий принцип так: чем больше формализованных доказательств, тем больше можно сделать новых.

Ограничения

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

Что делать на практике

Если вы строите агентные системы для кода, присмотритесь к Lean и идее проверяемых артефактов: пусть агент выдаёт не только код, но и то, что проверяется автоматически. Для продактов вывод проще: «ИИ написал» и «ИИ написал и это доказано» скоро станут двумя разными категориями качества. Тем, кто работает в критичных областях — финансы, медицина, безопасность, — этот сдвиг стоит держать на радаре уже сейчас.