Axiom открыла 16-миллионную библиотеку по алгебраической геометрии, созданную ИИ-агентами
Компания заявляет, что агенты формализовали в Lean весь пригодный для формализации материал Stacks Project; код ИИ отделён от проверенного людьми слоя.
Axiom открыла формализацию Stacks Project на языке Lean — большого справочника по алгебраической геометрии. По данным компании, библиотека содержит около 16 млн строк и охватывает все теги проекта, материал которых можно формализовать.
В отличие от доказательства одной теоремы, релиз задуман как переиспользуемая инфраструктура. Исследователи могут импортировать библиотеку, изучать зависимости и строить поверх неё новые результаты с машинной проверкой. Axiom утверждает, что иерархическая система специализированных ИИ-агентов переводила утверждения, искала подходящие абстракции в Mathlib, строила доказательства и разрешала зависимости по всему графу проекта.
Ядро Lean проверяет доказательства, а репозиторий заявляет, что в них нет заглушек sorry и обходов через native_decide. Во время работы система, по словам Axiom, обнаружила десятки утверждений, которым потребовались локальные уточнения: например, недостающие условия и граничные случаи в положительной характеристике.
Это не означает, что весь перевод уже прошёл независимую математическую проверку. В репозитории проверенные людьми модули StacksCore отделены от написанных ИИ модулей StacksFrontier, которым ещё нужна ревизия. Заявление о крупнейшей интегрированной переиспользуемой библиотеке формальной математики также принадлежит самой Axiom. Даже с этими оговорками проект показывает, что согласованная группа агентов может создавать проверяемое научное ПО в масштабе целой области, а не одной теоремы.
