Axiom выпустила формализацию Stacks Project в Lean: около 16 млн строк

Axiom выпустила формализацию на языке Lean всего Stacks Project, открытого справочника объёмом примерно 7500 страниц, на котором строятся основы современной алгебраической геометрии. По словам компании, получилась библиотека примерно в 16 млн строк кода, и это крупнейшая интегрированная библиотека формализованной математики из всех созданных. Теперь весь математический материал проекта доступен как единая библиотека, проверенная машиной. Исследователи и ИИ-агенты могут импортировать её определения и теоремы в новые формальные доказательства, а постоянные теги Stacks связывают каждое объявление в Lean с каноническим текстом, который математики уже знают.

Stacks Project начал в 2005 году математик из Колумбийского университета Йохан де Йонг. Из введения в алгебраические стеки он вырос в живую совместную энциклопедию, где тысячи постоянных четырёхсимвольных тегов. Принципы проекта строгие: у каждой теоремы есть доказательство, каждое допущение названо явно, каждый шаг указывает на теги, от которых зависит. Axiom подчёркивает, что работа опирается и на сообщества Lean и Mathlib, которые годами строили математическую библиотеку и нужные абстракции.

Зачем это нужно, объясняет сама компания. ИИ-системы всё чаще порождают математические аргументы быстрее, чем люди успевают их проверять, поэтому формальная верификация становится необходимой. В областях с развитой инфраструктурой Lean новые результаты часто формализуют вскоре после открытия, а современная алгебраическая геометрия до сих пор поддавалась этому плохо: одно доказательство может опираться на длинную цепочку теорем из коммутативной алгебры, схем, пучков, когомологий и алгебраических стеков. Математика была в Stacks Project, а соответствующей инфраструктуры Lean не было.

Axiom называет задачу в той же мере инженерной, что и математической. Бесконтрольная генерация кода ИИ быстро даёт короткие изолированные скрипты, но для миллионов строк проверенной математики нужны чистые абстракции и стабильные интерфейсы. Если тысячи агентов доказывают теоремы параллельно без архитектурной координации, два агента могут доказать верные теоремы об одном объекте с несовместимыми определениями или продублировать то, что уже есть в Mathlib. Ядро Lean примет оба файла по отдельности, но собрать их результаты потом будет крайне трудно. Поэтому математики и инженеры Axiom спроектировали иерархическую систему ИИ-агентов с разделением обязанностей и строгими протоколами координации. Агенты параллельно по графу зависимостей переводили утверждения, искали готовые абстракции в Mathlib, строили доказательства и закрывали предпосылки, согласуя определения, интерфейсы классов типов и абстракции между главами.

Верность формулировок, по словам компании, важнее самого доказательства, поэтому её проверяют автоматически: аудитом несколькими агентами, семантическими сверками с исходным текстом и жёстким требованием, чтобы каждое определение и лемма стыковались с зависящими от них теоремами. Дополнительно проводятся выборочные аудиты базовых определений и знаковых теорем.

В ходе работы система выявила десятки утверждений Stacks Project, которым требовалось локальное уточнение: пропущенные гипотезы, особые случаи в положительной характеристике и утверждения, не верные в заявленной общности. Агенты определяли причину неудачных попыток доказательства и строили явные контрпримеры, показывающие, где исходные утверждения не работают. Для локальных упущений они находили недостающие гипотезы и формализовали исправленные теоремы вместе с контрпримерами. Если ложная вспомогательная лемма оставляла брешь в доказательстве более глубокой теоремы, агенты находили в литературе обходные пути и доказывали главный результат при исходных гипотезах.

На сайте stacks.axiommath.ai страницы оригинального Stacks Project можно смотреть рядом с соответствующим кодом Lean и изучать интерактивный граф зависимостей. Один тег Stacks часто раскрывается в несколько формальных определений и лемм: часть новых, часть связана с уже существующими объявлениями Mathlib, и интерфейс показывает эти соответствия явно. Ранее, 27 октября 2026 года, Axiom выпустила формализацию классификации конечных простых групп (CFSG); та работа выстроена вокруг одной знаковой теоремы, а Stacks Project, это библиотека для многократного использования.

Отдельно Axiom описывает границу с авторами оригинала. В объявлении от 21 октября 2026 года де Йонг попросил пока не отправлять сгенерированные ИИ комментарии и pull request напрямую в основной репозиторий Stacks Project. Stacks Project остаётся живым текстом под управлением де Йонга и сообщества, а формализация на Lean, независимый открытый проект, который ведёт Axiom. Компания пишет, что уважает эту границу и держит формализацию, контрпримеры и уточнения в собственном репозитории.

Ключевые факты

• Axiom выпустила формализацию на Lean всего Stacks Project (около 7500 страниц по алгебраической геометрии); по её словам, это около 16 млн строк кода и крупнейшая интегрированная библиотека формализованной математики.
• Работу, по описанию Axiom, выполнили скоординированные «рои» ИИ-агентов с иерархией, специализацией и строгими протоколами координации: они параллельно переводили, доказывали и встраивали тысячи теорем.
• Система выявила десятки утверждений Stacks Project, требующих уточнения: пропущенные гипотезы, особые случаи в положительной характеристике, утверждения не в заявленной общности; для части из них построены явные контрпримеры.
• Постоянные теги Stacks связывают каждое объявление Lean с оригинальным текстом; на stacks.axiommath.ai можно смотреть страницы рядом с кодом и изучать интерактивный граф зависимостей.
• Де Йонг 21 октября 2026 года попросил пока не присылать сгенерированные ИИ комментарии и pull request в основной репозиторий; Axiom держит формализацию и уточнения в собственном репозитории.

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

Современная алгебраическая геометрия опирается на длинные цепочки теорем, и формализовать новое доказательство в ней было трудно: не хватало инфраструктуры Lean. Axiom утверждает, что теперь база готова, и по её оценке это крупнейшая библиотека формализованной математики. Второй сюжет, побочный результат: формализация, по словам компании, нашла десятки мест в уважаемом справочнике, где утверждения требовали уточнения. Это пример того, как машинная проверка может усиливать саму математическую литературу. Третье, сам способ: Axiom описывает не разовые скрипты, а согласованную работу множества ИИ-агентов над единой кодовой базой в миллионы строк.

Кому это важно

Математикам, работающим в алгебраической геометрии и смежных областях, как возможность опираться на проверенные определения и теоремы. Разработчикам и исследователям формальной верификации, пользователям Lean и Mathlib, как крупный пример совместимой библиотеки. Тем, кто строит многоагентные системы для больших кодовых баз: Axiom подробно описывает проблему несовместимых определений при параллельной работе агентов и её решение через иерархию и протоколы координации.

Как это применить

Согласно Axiom, определения и теоремы библиотеки можно импортировать в новые формальные доказательства: например, при формализации теоремы о семействах кривых не придётся заново строить основы схем или когерентных когомологий. Ядро Lean при этом допускает применение результата, только если выполнены его точные гипотезы. Для навигации служит сайт stacks.axiommath.ai: страницы оригинального проекта рядом с кодом Lean и интерактивный граф зависимостей. Библиотека и контрпримеры хранятся в репозитории Axiom, где с ними могут ознакомиться математики.

Можно ли доверять

Источник, собственная публикация Axiom, то есть заявления разработчика о своей работе. Оценка «крупнейшая библиотека формализованной математики из всех созданных», слова самой компании. В тексте не названы модели, число агентов, затраты вычислений и сроки, не перечислены найденные десятки уточнений, а независимая проверка или реакция сообществ Lean и Mathlib не приводятся. Достоверность формулировок, по описанию Axiom, обеспечивается автоматическим аудитом несколькими агентами, семантическими сверками и проверкой стыковки с зависящими теоремами; доказательства при этом проверяет ядро Lean.

Риски и подводные камни

Главный вопрос, соответствие формальных утверждений исходному смыслу: Axiom сама называет его более важным, чем проверку доказательства, и решает его автоматическим аудитом, дополненным выборочными проверками. Заявленные ошибки и уточнения оригинала пока подтверждаются лишь описанием компании. Есть и организационный момент: де Йонг пока просит не слать сгенерированные ИИ комментарии и pull request в основной репозиторий Stacks Project, поэтому найденные уточнения живут отдельно, в репозитории Axiom, и сами по себе в оригинал не попадают. Формализация, независимый проект, который поддерживает Axiom, а не часть Stacks Project.

«Убедиться, что каждое формальное утверждение достоверно передаёт математический смысл исходного текста, ещё важнее, чем проверить его доказательство.»

— Axiom, блог компании