Axiom Math перевела Stacks Project в Lean: 7 500 страниц математики для проверки машиной

Раньше исследователю приходилось заново строить нужные основы в системе формальных доказательств. Теперь он может взять определения и теоремы Stacks, например для работы с семействами кривых.

Не хотите разбираться сами? Внедряем ИИ в ваш бизнес: задачи без лимита, одна цена в месяц, отмена в любой момент.

Два уровня проверки. В StacksCore люди проверили соответствие формулировок исходнику и стандартам Mathlib. StacksFrontier написали ИИ-агенты, и эта часть ещё ждёт такого ревью. Lean проверяет корректность доказательства записанного утверждения. Соответствует ли оно исходной математической задаче, люди проверяют отдельно.

Axiom поручила системе агентов параллельно переводить формулировки и строить доказательства, согласуя зависимости между главами. По данным компании, агенты нашли десятки утверждений, которым потребовались уточнения: строили контрпримеры и добавляли недостающие условия.

Как использовать. На сайте Stacks Project in Lean можно найти теорему по постоянному четырёхсимвольному тегу, открыть Lean-код и посмотреть зависимости. В проекте Lean команда `import Stacks` подключает обе части библиотеки. Команда `#stacks_tags!` выводит объявления с тегами и формулировками.

Исходники доступны в AxiomMath/Stacks. Для сборки README от 4 ноября указывает Lean 4 v4.34.0-rc2 и команды `lake exe cache get`, затем `lake build`. В библиотеке около 63 000 модулей, поэтому полная сборка требует много времени и памяти. Команда загрузки кэша скачивает готовые сборки Mathlib, кэш самой Stacks пока запланирован.

Первоисточник: [TechCrunch, 5 ноября 2026 года](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics).

Для новой формализации или ревью сначала нужен claim с blueprint и метка `blueprint-approved`, а небольшие исправления принимаются сразу через PR.