Axiom Math формализовала Stacks Project — открытую библиотеку математических результатов, созданную в 2005 году. Около 7654 страниц проекта перевели примерно в 16 млн строк кода на языке Lean.
Lean проверяет математические доказательства построчно с помощью proof assistant. Такой подход позволяет проверять логическую корректность доказательств, а не только их правдоподобие.
Stacks Project охватывает темы от университетской алгебры до алгебры, геометрии и теории чисел. Его определения и теоремы связаны между собой, поэтому при формализации нужно было сохранить зависимости между результатами.
ИИ-агенты Axiom Math работали параллельно и сами выбирали задачи внутри заданной структуры проекта. Компания также обучала собственные модели работе с математикой и Lean.
По словам команды, формализация закрывает заметный пробел в существующей базе проверенной математики: до этого в Lean было мало материалов по алгебраической геометрии. Теперь новые доказательства в этой области можно строить на уже проверенных результатах.
Axiom Math рассчитывает использовать проверенные библиотеки как основу для ИИ-агентов, которые пишут программный код и создают новые инструменты. Компания считает, что такой подход поможет снизить риск ошибок в системах, создаваемых ИИ.
