Создаётся впечатление, что искусственный интеллект почти каждую неделю решает новую математическую задачу. В прошлом месяце только OpenAI опубликовала 719 препринтов, утверждая, что решила некоторые из самых сложных проблем в этой области. Даже проверка с помощью компьютера может содержать ошибки. После многих лет искусственного интеллекта, генерирующего мусор, возникает вопрос: не станет ли математика следующей областью, затронутой этим явлением?
AxiomMath может избежать такой судьбы, не замедляя темпы, а создав более прочную основу. Эта стартап-компания с оценкой в 1,6 млрд долларов стремится создать проверенный базовый уровень, на котором могут полагаться AI-агенты для написания программного обеспечения и в конечном итоге проведения научных исследований.
В среду компания объявила, что официально подтвердила проект Stacks — одно из крупнейших математических достижений, написанных человеком. Математики обычно высоко оценивают Stacks. Математик из Колумбийского университета Питер Вoit назвал его «едва ли есть что-либо, что могло бы с ним сравниться», и сравнил этот проект с «знаменитой серией книг Bourbaki» — серией работ, перестроившей математику с основ в XX веке.
Коллега Войта из Колумбии Йохан де Йонг запустил проект Stacks в 2005 году в качестве открытого справочного материала. С тех пор математики вносят в него вклад, расширяя его от университетского уровня алгебры до самых передовых идей в области алгебры, геометрии и теории чисел.
Группа ИИ-агентов компании перевела эту базу данных из примерно 7 654 страниц в примерно 16 миллионов строк кода, проверяемого компьютером.
Цель формализованной математики — обеспечить надежность ее базовой структуры. Математики переписывают доказательства в виде кода с использованием языка программирования под названием Lean, а затем программа-ассистент доказательств проверяет этот код построчно. Если доказательство проходит проверку, математики могут быть уверены, что оно логически корректно.
Инженеры также используют ту же идею — формальную верификацию — для проверки жизнеспособности проектирования чипов; французские исследователи применили её для обнаружения уязвимости в программном обеспечении для расчета семейных пособий.
Для таких репозиториев, как Stacks Project, проверка теорем по одной является лишь частью работы. Теоремы и определения в Stacks взаимосвязаны, и каждая из них строится на предыдущих. Как в генеалогическом древе, многие результаты в Stacks можно проследить до более ранних результатов.
Эта взаимосвязанность заставила Axiom сначала сомневаться в жизнеспособности проекта. Команда должна была сохранить все соединения целыми в примерно 16 миллионах строк кода Lean.
Генеральный директор Axiom Карина Хонг сказала TechCrunch: «В реальности крупный масштаб и точность обычно несовместимы. [Stacks] — это набор математических результатов, составляющих математическую основу. Вы хотите, чтобы [теоремы] были согласованы между собой, а не противоречили друг другу. Вы также хотите, чтобы эти определения не конфликтовали друг с другом.»
Этот 25-летний генеральный директор бросил программу докторантуры по математике в Стэнфордском университете и основал эту компанию в марте 2025 года. В марте этого года Axiom привлекла 200 миллионов долларов в серии A, возглавляемой Menlo Ventures.
Хонг сказал: «Мы тогда не были уверены, сможем ли мы сохранить эстетику Stacks в vibe coding».
Для завершения этого проекта команда предоставила агентам гибкую структуру и запустила их параллельно. Ашвин Сваминатхан, член команды Axiom Technology, сказал: «Для Stacks мы установили иерархию… но не такую, в которой строго определено, что должен делать каждый агент. Агенты сами находят задачи и определяют, что можно обрабатывать параллельно».
Axiom также обучила свои модели, чтобы они хорошо справлялись с математикой. Хонг говорит, что этот подход не используется большинством других стартапов в области верификации. Изначально команда полагалась на внутреннего эксперта по методологии Lean, чтобы научить агентов формировать суждения, подобные человеческим. Со временем, по словам Хонга, эти агенты научились этому самостоятельно.
Этот результат заполнил одну из крупнейших пробелов в формальной математике. Сваминатан говорит: «Когда вы смотрите на уже формализованный математический контент, вы замечаете огромную черную дыру. И эта черная дыра охватывает алгебраическую геометрию».
Сваминатан сказал, что до сих пор исследователям, желающим использовать Lean для проверки новых работ в алгебраической геометрии, практически не было доступно готовой базы. «Теперь у них есть».
Axiom считает, что каждая проверенная работа становится строительным блоком, на котором будущие доказательства могут основываться на уже проверенной математике, не начиная с нуля. Математик из UCLA, лауреат Филдсовской премии Теренс Тао сформулировал это более кратко: «Чем больше у вас формализованных доказательств, тем больше вы сможете создать формализованных доказательств».
Целевая аудитория Axiom — это не только математики. Разработчики долгое время стремились обеспечить отсутствие уязвимостей и безопасность своего кода. По мере того как AI-агенты пишут все больше программного обеспечения, эта проблема будет только расти.
Axiom ставка: будущее программное обеспечение должно строиться на проверенных основах, как сегодня Stacks.
Сваминатан говорит: «Мы считаем, что математика — это область, с которой вы начинаете создавать эти вещи, и это переносимый навык. Агенты могут читать наш код, понимать его и строить на нем новую инфраструктуру. То, что мы формализовали с помощью Lean, теперь служит фундаментом, на котором агенты могут строить».
Способ, которым Axiom строит агентов для Stacks — параллельная работа и самостоятельный выбор задач — именно то, как Хонг предполагает, что многие AI-задачи будут выполняться в будущем. Она считает, что AI-агентам необходима хорошо структурированная и многократно используемая база знаний, чтобы избежать генерации мусора.
Хонг говорит: «Вы хотите, чтобы [агент] имел переиспользуемую базу, на которой он мог бы продолжать строить и постоянно расширять границы. Если изначально засорить её плохими инженерными решениями, то расширить эти границы будет крайне сложно».
Хонг очень уверена в этом методе и даже публично бросила вызов. Она сказала: «Я публично вызываю все программные компании выполнить формализацию такого масштаба».