Axiom опубликовала формализацию всего Stacks Project на Lean. Оригинальный открытый справочник по алгебраической геометрии, начатый математиком Колумбийского университета Йоханом де Йонгом в 2005 году, занимает примерно 7500 страниц. По заявлению Axiom, формальная версия охватывает около 16 млн строк кода и является крупнейшей интегрированной reusable-библиотекой формализованной математики.
Определения и теоремы можно импортировать в новые доказательства, а Lean kernel проверяет соблюдение точных предпосылок. Постоянные четырёхсимвольные Stacks tags связывают Lean declarations с каноническим текстом. На stacks.axiommath.ai исходные страницы показаны рядом с формальным кодом, доступны dependency graph и сопоставления одного тега с несколькими определениями или lemmas, включая связи с Mathlib.
В отличие от формализации Classification of Finite Simple Groups вокруг одной крупной теоремы, Stacks Project представляет собой фундаментальную библиотеку взаимосвязанных определений и результатов. Она охватывает commutative algebra, schemes, sheaves, cohomology и algebraic stacks. Исследователю или AI-агенту больше не нужно заново восстанавливать эту инфраструктуру для каждой новой теоремы.
Axiom использовала координированные иерархии AI-агентов со специализированными ролями. Они параллельно переводили утверждения, искали существующие абстракции Mathlib, строили доказательства и разрешали prerequisites. Математики и инженеры задавали общие interfaces и coordination protocols, чтобы независимо проверенные файлы не использовали несовместимые определения одного объекта.
По описанию команды, соответствие формальных утверждений оригиналу проверялось multi-agent auditing, semantic cross-checks и обязательной совместимостью с downstream теоремами. Дополнительные целевые аудиты касались базовых определений и важнейших результатов. Независимой оценки всей библиотеки в публикации нет, поэтому заявления о масштабе и полноте принадлежат Axiom.
Формализация выявила десятки утверждений, потребовавших локального уточнения: пропущенные гипотезы, edge cases в positive characteristic и слишком общие формулировки. Агенты строили counterexamples, добавляли исправленные версии теорем, а для более глубоких результатов иногда искали альтернативные доказательства в литературе.
Проект Axiom независим от upstream Stacks Project. 21 октября де Йонг попросил временно не отправлять AI-generated comments и pull requests напрямую в исходный репозиторий. Axiom оставляет формализацию, counterexamples и уточнения в собственном open-source репозитории для проверки математическим сообществом.