Как сообщает TechCrunch, стартап AxiomMath объявил, что полностью формально верифицировал Stacks Project — одно из крупнейших собраний математических текстов, когда-либо написанных людьми. Флот ИИ-агентов компании перевёл около 7 654 страниц справочника в примерно 16 млн строк машинно-проверяемого кода на языке Lean.
Stacks Project запустил в 2005 году математик Колумбийского университета Йохан де Йонг как открытый справочник: от алгебры студенческого уровня до передовых результатов в алгебраической геометрии и теории чисел. Его коллега Питер Воит говорил, что «по-настоящему сопоставимого больше нет», и сравнивал проект со знаменитыми книгами Бурбаки, которые в XX веке перестроили математику с самых основ.
Формальная верификация — это переписывание доказательств в виде кода, который построчно проверяет специальная программа, ассистент доказательств. Тот же принцип инженеры применяют для проверки конструкций чипов. Сложность Stacks в том, что его теоремы и определения опираются друг на друга, и все эти связи команде AxiomMath пришлось сохранить на протяжении примерно 16 млн строк кода.
Гендиректору AxiomMath Карин Хонг 25 лет: она ушла из аспирантуры по математике Стэнфорда и основала компанию в марте 2025 года. В марте стартап привлёк $200 млн в раунде Series A под руководством Menlo Ventures, а TechCrunch называет AxiomMath компанией стоимостью $1,6 млрд. Компания также обучила собственные модели, ориентированные на математику, — подход, который, по словам Хонг, другие стартапы в верификации не применяли.
Проект появился на фоне растущего потока ИИ-контента в науке: как отмечает TechCrunch, только OpenAI за прошлый месяц выпустила 719 рукописей с заявленными решениями сложнейших математических задач. AxiomMath рассчитывает, что программы будущего будут опираться на проверенные основания — особенно по мере того, как всё больше кода пишут ИИ-агенты. «Чем больше формализованных доказательств у вас есть, тем больше формализованных доказательств вы можете сделать», — формулирует лауреат Филдсовской премии Теренс Тао.
Хонг напрямую бросила вызов конкурентам: «Открыто вызываю все компании, занимающиеся кодом, поработать над формализацией в таком масштабе».
