AxiomMath объявила о верификации Stacks Project — TechCrunch
Компания AxiomMath объявила о формальной верификации Stacks Project — крупной открытой библиотеки математических результатов. Как сообщает TechCrunch, ее ИИ-агенты перевели примерно 7 654 страницы проекта в около 16 миллионов строк кода Lean, проверенного компьютерным ассистентом доказательств.
Проверка математических доказательств
Формализация математики предполагает переписывание доказательств на языке программирования Lean. Специальная программа — ассистент доказательств — проверяет код строка за строкой. Если проверка проходит успешно, математики могут считать доказательство логически корректным.
Stacks Project был основан в 2005 году математиком Колумбийского университета Йоханом де Йонгом как открытый справочный ресурс. С тех пор математики дополняли его материалами — от университетской алгебры до сложных тем алгебры, геометрии и теории чисел. Математик Питер Войт сравнивал значение этого проекта с серией книг Бурбаки, которая в XX веке выстраивала математику с ее основ.
Сложность работы заключалась не только в проверке отдельных теорем. Определения и результаты в Stacks Project связаны между собой, поэтому команде требовалось сохранить все связи при работе примерно с 16 миллионами строк кода Lean.
Больше актуальных новостей — в Telegram-канале UA.News Telegram.
Основа для новых доказательств
Представитель технической команды AxiomMath Ашвин Сваминатан заявил, что результат заполняет большой пробел в формализованной математике, в частности в алгебраической геометрии. По его словам, исследователи, которые хотят проверять новые работы в этой области с помощью Lean, теперь имеют основу для такой работы.
Компания считает, что проверенные математические результаты могут быть повторно используемыми блоками для новых доказательств и основой для инфраструктуры, с которой будут работать ИИ-агенты. Основательница и генеральный директор Карина Хонг заявила, что агентам необходима надежная библиотека знаний, чтобы развивать ее без ошибок, заложенных неудачными инженерными решениями на начальных этапах.
Хонг основала компанию в марте 2025 года после того, как ушла из докторской программы по математике в Стэнфорде. В марте AxiomMath привлекла $200 миллионов в раунде Series A, который возглавила Menlo Ventures.
