Axiom Math формально проверила Stacks Project с помощью ИИ-агентов

Axiom Math заявила, что ее ИИ-агенты формально проверили Stacks Project — крупную открытую математическую библиотеку, которую Johan de Jong начал создавать в 2005 году. В ней собраны результаты по алгебре, геометрии и теории чисел, добавленные многими математиками. Математик из Columbia Peter Woit сравнивал проект по значимости с книгами Bourbaki.

Компания перевела примерно 7 654 страницы библиотеки примерно в 16 миллионов строк кода на Lean. Специальная программа, называемая proof assistant, проверяет код построчно и позволяет удостовериться в логической непротиворечивости доказательств. В случае Stacks требовалось сохранить связи между определениями и теоремами: многие результаты опираются на предыдущие элементы библиотеки.

Генеральный директор Axiom Carina Hong рассказала, что агенты работали параллельно в рамках общей иерархии и самостоятельно находили подходящие задачи. Компания также обучила собственные модели математике. В Axiom считают, что готовая формализация даст исследователям основу для работы с алгебраической геометрией, где ранее было мало материалов на Lean. Стартап основан в марте 2025 года; в марте он привлек $200 миллионов в раунде Series A под руководством Menlo Ventures. Компания также рассматривает проверенную математику как основу для программного обеспечения, создаваемого ИИ-агентами.