Axiom Math не хочет пускать ИИ-шлак в математику

Что такое Stacks Project

Проект начал в 2005 году Джохан де Йонг, коллега математика Колумбийского университета Питера Войта. Это открытый справочник, который математики пополняли годами. Войт сравнивал его с книгами Бурбаки — серией, которая в XX веке заново выстроила математику на фундаментальных основаниях, — и говорил, что Stacks Project трудно с чем-либо сопоставить.

AxiomMath — стартап стоимостью $1,6 млрд — объявила о завершении формальной проверки проекта в среду. Компания перевела библиотеку примерно из 7 654 страниц в около 16 млн строк кода на языке Lean. Её агенты выполняли работу параллельно.

Формальная проверка превращает математическое доказательство в код. Математики записывают его на Lean, а программа-помощник доказательств проверяет код строка за строкой. Если проверка пройдена, доказательство можно считать логически корректным. Тот же подход инженеры применяют, чтобы проверять работу проектов микросхем; исследователи во Франции использовали его для поиска ошибок в программе расчёта семейных пособий.

Почему важны связи между результатами

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

Из-за этих связей в AxiomMath поначалу сомневались, получится ли формализовать весь проект. Команде нужно было сохранить каждую связь в массиве примерно из 16 млн строк кода. Глава компании Карина Хонг объясняла, что в такой математической базе особенно важно не допустить противоречий между теоремами и определениями.

Хонг, которой 25 лет, оставила докторскую программу по математике в Стэнфордском университете и основала компанию в марте 2025 года. В марте AxiomMath привлекла $200 млн в раунде серии A под руководством Menlo Ventures.

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

Компания также обучила собственные модели математике. Хонг отмечала, что большинство других стартапов в области формальной проверки этого не делали. Сначала агенты учились у специалиста AxiomMath по Lean — перенимали человеческое чувство математического вкуса. Со временем, по словам Хонг, они начали вырабатывать его самостоятельно.

Основа для алгебраической геометрии

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

AxiomMath рассчитывает, что каждое проверенное утверждение станет строительным блоком для следующих доказательств: математикам не придётся начинать с нуля, а можно будет опираться на уже проверенные результаты. Математик Калифорнийского университета в Лос-Анджелесе и лауреат Филдсовской премии Теренс Тао сформулировал общий принцип: чем больше доказательств формализовано, тем больше новых доказательств можно формализовать.

Зачем проверенная математика разработчикам

Компания видит аудиторию проекта не только среди математиков. Разработчикам давно трудно гарантировать, что в программном коде нет ошибок и уязвимостей, а по мере того, как ИИ-агенты пишут всё больше программ, эта задача становится сложнее.

AxiomMath рассчитывает, что программное обеспечение будущего будут строить на проверенной основе — как Stacks Project теперь опирается на формализованные результаты. Сваминатан считает, что математика подходит для создания таких основ, а полученный навык можно переносить в другие области: агенты могут читать код компании, понимать его и создавать поверх него новую инфраструктуру. Формализация на Lean, по его словам, становится базой, на которой агенты могут строить дальше.

Хонг ожидает, что ИИ-агенты будут выполнять всё больше задач параллельно и самостоятельно выбирать работу — так же, как при формализации Stacks Project. Чтобы не выдавать ненадёжный результат, им нужна переиспользуемая библиотека знаний, на которой можно строить новые решения. Если же в начале заложить неудачные инженерные решения, расширять такую основу будет сложно. Хонг призвала компании, разрабатывающие инструменты для программирования, заняться формализацией в таком масштабе.

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