Проблема выглядит с каждым месяцем острее: ИИ-модели генерируют математические «доказательства» в невероятных объёмах — только OpenAI выпустила за месяц 719 рукописей с якобы решениями сложнейших задач. Компьютерная проверка тоже может ошибаться. После лет накопления ИИ-шлака логично опасаться, что математика станет следующей жертвой. Axiom Math делает ставку на другой путь: не замедлиться, а встать на более твёрдый фундамент.
На этой неделе стартап объявил о формальной верификации проекта Stacks — одного из крупнейших собраний математики, когда-либо написанных людьми. Математики относятся к Stacks с редким почтением: профессор Columbia Питер Вовт говорит, что ему нет настоящих аналогов, сравнивая его с классическим Бурбаки, переписавшим математику с фундамента в XX веке. Проект Stacks начался в 2005 году как открытый справочник и с тех пор вобрал результаты от школьной алгебры до самых продвинутых областей геометрии и теории чисел.
Axiom перевела примерно 7654 страницы Stacks в около 16 миллионов строк кода, который можно проверить автоматически. Суть формализации в том, что математики переписывают доказательство на языке программирования Lean, и специальная программа ассистента проверяет каждую строку построчно. Если доказательство проходит проверку — можно быть уверенным, что оно логически корректно. Инженеры используют этот же метод (формальную верификацию) для проверки чипов, а французские исследователи ловили с его помощью баги в ПО для расчёта соцвыплат.
Главная сложность была в том, что теоремы и определения в Stacks связаны между собой как семейное дерево — каждая опирается на предыдущие. Команде Axiom пришлось сохранить все 16 миллионов связей в Lean-коде без единого разрыва. Как объяснила CEO компании Карина Хонг (ей 25, она бросила аспирантуру по математике в Стэнфорде и основала компанию в марте 2025), большое и деликатное просто не живут вместе. Стеки — это фундамент математики, и ты не можешь просто так допустить противоречие или парадокс в определениях.
Для решения проблемы команда дала ИИ-агентам свободу действий и запустила их параллельно. Вместо жёсткой иерархии задач агенты сами находили, что сделать, и работали независимо. Axiom также обучила собственные модели математике — это подход, который, по словам Хонг, другие стартапы верификации не практикуют. Вначале людям-экспертам по Lean приходилось учить агентов, но со временем те выработали собственное чувство вкуса. Результат закрывает огромную яму в формализованной математике: алгебраическая геометрия была совершенно не освещена. Теперь математики, проверяющие новые работы через Lean, наконец имеют на что опираться.
Но целевая аудитория Axiom — не только математики. Разработчики уже давно борются с гарантией отсутствия багов и уязвимостей в коде, а проблема растёт с тем, что ИИ-агенты пишут всё больше ПО. Axiom ставит на то, что ПО будущего должно опираться на верифицированные фундаменты, как Stacks сейчас. Если агенты учатся работать с проверенной математикой, они смогут понимать её и строить на основе этого новую инфраструктуру. Хонг даже открыто вызывает все кодинг-компании: «Работайте над формализацией в таком масштабе».
Для российского бизнеса это практически значимо прежде всего в области, где критична корректность вычислений и где использование ИИ для генерации логики уже перешла из экспериментов в рутину: финтех, инженерные системы, расчёты в госсфере. Если организация использует ИИ для написания чувствительного кода, верифицированный фундамент существенно снижает риск. Локально это же применимо к любому сложному ПО, которое критично должно быть правильным, но в России пока редко встречается культура формальной верификации.
Алексей Мартыненко
Главный редактор SPV News
Это не просто техническое достижение. Axiom впервые доказывает, что ИИ способен делать не только халтуру, но и скучную, но критически важную работу по привлечению хаоса к порядку. Верифицированный фундамент становится активом, который множит ценность всех будущих доказательств и программ, построенных на его основе. Механика работает — и вопрос теперь только в том, примут ли это стандартом.