Axiom Math формально верифицировала Stacks Project с помощью ИИ-агентов
Стартап Axiom Math объявил, что формально верифицировал Stacks Project, один из крупнейших математических трудов, написанных людьми. Команда ИИ-агентов перевела около 7 654 страниц текста примерно в 16 миллионов строк кода на языке Lean.
Главное в цифрах
- Объём проекта: около 7 654 страниц
- Размер кода на Lean: около 16 миллионов строк
- Серия A: $200 млн, лид Menlo Ventures
- Оценка стартапа: $1,6 млрд
Программа-ассистент доказательств проверила каждую строку кода. По словам компании, проверка позволяет убедиться, что доказательства логически корректны. Формальная верификация используется и инженерами, которые проверяют конструкции микросхем.
Главная сложность проекта состояла в связности. Теоремы и определения Stacks строятся одна на другой, поэтому при переводе требовалось сохранить все связи между ними. Axiom изначально не была уверена, что это получится.
Контекст
Stacks Project начал в 2005 году Йохан де Йонг как открытый справочник. Математики продолжали дополнять его, и проект охватывает алгебру, геометрию и теорию чисел: от университетского уровня до самых сложных идей. Колумбийский математик Питер Вуит сравнил его с известными книгами Бурбаки.
Аgenty работали параллельно и сами находили задачи, для которых им нужен был лишь общий каркас. По словам Ашвина Сваминатана из технического штаба Axiom, именно алгебраическая геометрия оставалась большой «чёрной дырой» в формализованной математике, и теперь исследователи получили на чём её строить.
Что это значит
Axiom утверждает, что каждый проверенный результат становится основой для будущих доказательств. Гендиректор компании Карина Хонг считает, что ИИ-агентам понадобится надёжная библиотека знаний, чтобы не производить непроверяемый мусор. Стартап в марте привлёк $200 млн в серии A под руководством Menlo Ventures при оценке $1,6 млрд.
