Axiom Math проверила библиотеку Stacks Project с помощью AI-агентов

Коротко

Axiom Math заявила о формальной проверке Stacks Project — одной из крупнейших собраний математики, созданных людьми.
Около 7 654 страниц библиотеки перевели примерно в 16 млн строк проверяемого компьютером кода.
Для проверки математические доказательства переписывают на языке программирования Lean, а специальная программа проверяет код построчно.
Стартап оценивается в $1,6 млрд и рассчитывает создать проверенную основу для AI-агентов, которые смогут писать программное обеспечение и в перспективе заниматься наукой.

Что произошло

Axiom Math объявила о формальной верификации Stacks Project — открытого математического справочника, созданного Johan de Jong в 2005 году. В нем собраны результаты от алгебры университетского уровня до передовых идей в алгебре, геометрии и теории чисел.

Команда компании использовала флот AI-агентов, чтобы преобразовать примерно 7 654 страницы Stacks Project в около 16 млн строк кода на Lean. По словам компании, проект удалось проверить, сохранив связи между взаимозависимыми теоремами и определениями.

Как работает проверка

Формализация математики предполагает переписывание доказательства в виде кода на языке Lean. Затем proof assistant проверяет этот код построчно; если проверка пройдена, доказательство считается логически корректным.

В Stacks Project отдельной проверки каждой теоремы недостаточно: теоремы и определения связаны между собой, а многие результаты опираются на более ранние. Именно эту взаимосвязанность Axiom Math пришлось сохранять в массиве кода.

Почему это важно

Axiom Math позиционирует формальную верификацию как способ создать более надежную основу для AI-агентов. Стартап рассчитывает использовать ее для разработки программного обеспечения и в перспективе для научной работы.

Интерес к проверке математических результатов усилился на фоне распространения непроверенных материалов, созданных с помощью AI. В прошлом месяце OpenAI выпустила 719 рукописей, заявляющих о решениях некоторых самых сложных задач математики.

Контекст

Stacks Project развивается как открытый справочник с 2005 года. Математик Peter Woit из Columbia сравнивал его с серией Bourbaki и говорил, что ему трудно найти сопоставимый проект.

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